Faculty

Pavol Černý
Bor-Yuh Evan Chang
Dirk Grunwald
Sriram Sankaranarayanan
Fabio Somenzi

Students

PhD

Sam Blackshear
Aleksandar Chakarov
Devin Coughlin
Arlen Cox
Jedidiah McClurg
Thomas Nelson
Hadi Ravanbakhsh
Yi-Fan Tsai
Michael Vitousek
Chris Wailes
Yan Zhang
Aditya Zutshi

BS/BA+MS

Kira Quan

BS/BA

Paul Givens
Nathan Lapinksi

Alumni

Faculty

Amer Diwan
Jeremy G. Siek

PhD

Geoffrey Belter
Justin E. Gottschlich
Ian Karlin
Weiyu Miao
Todd Mytkowicz
Christoph Reichenbach

BS/BA+MS

Erik Silkensen

MS

Neelam Agrawal
Huck Bennett
Shashank Bharadwaj
Jonathan Turner

BS/BA

Alex Beal
Nicholas Vanderweit

Affiliates

2014.10.24:
Devin Coughlin comes in second at the SPLASH-SRC 2014.
2014.10.16:
Aditya Zutshi and Sriram Sankaranarayanan receive the best paper award for their paper "Multiple Shooting, CEGAR-based Falsification for Hybrid Systems" at EMSOFT 2014.
2014.10.15:
Please consider applying or encourage your students and postdocs to apply for a tenure-track position in the Department of Computer Science at the University of Colorado Boulder. We have multiple openings with one particular interest area being secure and reliable software systems. Applications will be evaluated beginning on December 1, 2014, will continue until the position is filled, and are to be submitted on-line at http://www.jobsatcu.com/postings/89652.
2014.10.02:
Christos Dimoulas from Harvard is visiting us on October 7, 2014. He is giving a CUPLV Seminar entitled "Behavioral contracts and security" at 11:00am in ECCR 151 on Tuesday, October 7, 2014.
2014.09.12:
Aleksandar Chakarov wins the Radhia Cousot Young Researcher Best Paper Award at SAS 2014 for his paper "Expectation Invariants for Probabilistic Program Loops as Fixed Points" co-authored with Sriram Sankaranarayanan.
2014.07.10:
There is a postdoctoral research associate position open with the opportunity to work with Profs. Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Pavol Černý. Highly-qualified candidates may be considered for a research assistant professor position.
2014.07.10:
Eric Schkufza from Stanford is visiting us on July 15, 2014. He is giving a CUPLV Seminar entitled "Stochastic Optimization of x86_64 Binaries" at 11:00am in KOBL 300 on Tuesday, July 15, 2014.
2014.06.27:
CUPLV authors Hadi Ravanbakhsh, Aditya Zutshi, and Sriram Sankaranarayanan with collaborators have had papers accepted for presentation at EMSOFT 2014 in October (Ravanbakhsh and Sankaranarayanan, and Zutshi et al.).
2014.06.01:
CUPLV authors Aleksandar Chakarov, Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan with collaborators have had papers accepted for presentation at SAS 2014 in September (Chakarov and Sankaranarayanan, Cox et al., and Toubhans et al.).
2014.04.18:
CUPLV authors Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan have had a paper "QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers" accepted for presentation at CAV 2014 in July.
2014.02.19:
S-Taliro developed by Sriram Sankaranarayanan and collaborators receives press coverage in Embedded Computing Design.
2014.02.19:
Prospective Ph.D. students visit February 21. Welcome!
2014.02.03:
Sam Blackshear is one of only eleven winners of a 2014-2015 Facebook Graduate Fellowship!
2014.02.05:
CUPLV author Sam Blackshear with collaborators have had a paper "Verification Modulo Versions: Towards Usable Verification" accepted for presentation at PLDI 2014 in June.
2014.10.24: Devin Coughlin comes in second at the SPLASH-SRC 2014.
2014.10.16: Aditya Zutshi and Sriram Sankaranarayanan receive the best paper award at EMSOFT 2014.
2014.10.15: Multiple tenure-track openings in CS, including in secure and reliable software systems.
2014.10.02: Christos Dimoulas visits October 7.
2014.09.12: Aleksandar Chakarov wins the Radhia Cousot Young Researcher Best Paper Award at SAS 2014.
2014.07.10: Call for Postdoc applicants for Fall 2014.
2014.07.10: Eric Schkufza visits July 15.
2014.06.27: Two papers with CUPLV authors accepted to EMSOFT 2014! [1, 2]
2014.06.01: Three papers with CUPLV authors accepted to SAS 2014! [1, 2, 3]
2014.04.18: Paper by Cox et al. accepted to CAV 2014.
2014.02.19: Press coverage on S-Taliro in Embedded Computing Design.
2014.02.19: Prospective Ph.D. students visit February 21. Welcome!
2014.02.05: Paper by Logozzo et al. accepted to PLDI 2014.
2014.01.22: Devin Coughlin presenting at POPL 2014 today.
Ph.D. Positions. We are looking for strong students to join our diverse and dynamic group in programming languages and verification. Application deadline is December 15, 2014.
Postdoc Position. There is a postdoctoral research associate position open with the opportunity to work with Profs. Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Pavol Černý. Highly-qualified candidates may be considered for a research assistant professor position.

Projects

QUIC GraphsRelational Invariant Generation for Containers
ThresherPrecise Refutations for Heap Reachability
Fissile Type AnalysisModular Checking of Almost-Everywhere Invariants

Recent Publications

EMSOFT 2014New Delhi, IndiaOctober 2014

2014
Infinite Horizon Safety Controller Synthesis through Disjunctive Polyhedral Abstract Interpretation
Hadi Ravanbakhsh and Sriram Sankaranarayanan
EMSOFT 2014: International Conference on Embedded Software
2014
Multiple Shooting, CEGAR-based Falsification for Hybrid Systems
Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy V. Deshmukh, and James Kapinski
EMSOFT 2014: International Conference on Embedded Software

SAS 2014Munich, GermanySeptember 2014

2014
Expectation Invariants for Probabilistic Program Loops as Fixed Points
Aleksandar Chakarov and Sriram Sankaranarayanan
SAS 2014: International Static Analysis Symposium
2014
Automatic Analysis of Open Objects in Dynamic Language Programs
SAS 2014: International Static Analysis Symposium
2014
An Abstract Domain Combinator for Separately Conjoining Memory Abstractions
SAS 2014: International Static Analysis Symposium

CAV 2014Vienna, AustriaJuly 2014

2014
QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
CAV 2014: International Conference on Computer Aided Verification

PLDI 2014Edinburgh, UKJune 2014

2014
Verification Modulo Versions: Towards Usable Verification
PLDI 2014: ACM SIGPLAN Conference on Programming Language Design and Implementation

CHI-EA 2014Toronto, Ontario, CanadaApril 2014

2014
Android Apps Consistency Scrutinized
Khalid Alharbi, Sam Blackshear, Emily Kowalczyk, Atif Memon, Bor-Yuh Evan Chang, and Tom Yeh
CHI-EA 2014: Extended Abstracts at ACM SIGCHI Conference on Human Factors in Computing Systems

POPL 2014San Diego, California, USAJanuary 2014

2014
Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants
POPL 2014: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2014
Abstract Acceleration of General Linear Loops
POPL 2014: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages

VMCAI 2014San Diego, California, USAJanuary 2014

2014
Refuting Heap Rechability (Extended Abstract)
VMCAI 2014: International Conference on Verification, Model Checking, and Abstract Interpretation

SAIRP 2013Manhattan, Kansas, USASeptember 2013

2013
Modular Construction of Shape-Numeric Analyzers
SAIRP 2013: Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday

CAV 2013Saint Petersburg, RussiaJuly 2013

2013
Efficient Synthesis for Concurrency using Semantics-Preserving Transformations
Pavol Černý, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach
CAV 2013: International Conference on Computer Aided Verification
2013
Probabilistic Program Analysis with Martingales
Aleksandar Chakarov and Sriram Sankaranarayanan
CAV 2013: International Conference on Computer Aided Verification
2013
Flow*: An Analyzer for Non-Linear Hybrid Systems
Xin Chen, Erika Abraham, and Sriram Sankaranarayanan
CAV 2013: International Conference on Computer Aided Verification

ECOOP 2013Montpellier, FranceJuly 2013

2013
QUIC Graphs: Relational Invariant Generation for Containers
ECOOP 2013: European Conference on Object-Oriented Programming

LICS 2013New Orleans, Louisiana, USAJune 2013

2013
Regular Real Analysis
LICS 2013: IEEE Symposium on Logic in Computer Science

PLDI 2013Seattle, Washington, USAJune 2013

2013
Thresher: Precise Refutations for Heap Reachability
PLDI 2013: ACM SIGPLAN Conference on Programming Language Design and Implementation
2013
Almost-Correct Specifications: A Modular Semantic Framework for Assigning Confidence to Warnings
PLDI 2013: ACM SIGPLAN Conference on Programming Language Design and Implementation
2013
Towards Static Analysis for Probabilistic Programs
Sriram Sankaranarayanan, Aleksandar Chakarov, and Sumit Gulwani
PLDI 2013: ACM SIGPLAN Conference on Programming Language Design and Implementation

ICSE-NIER 2013San Francisco, California, USAMay 2013

2013
Exploring the Internal State of User Interfaces by Combining Computer Vision Techniques with Grammatical Inference
Paul Givens, Aleksandar Chakarov, Sriram Sankaranarayanan, and Tom Yeh
ICSE-NIER 2013: New and Emerging Results Track at ICSE
2013
Quantitative Abstraction Refinement
Pavol Černý, Thomas A. Henzinger, and Arjun Radhakrishna
POPL 2013: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages

VMCAI 2013Rome, ItalyJanuary 2013

2013
Reduced Product Combination of Abstract Domains for Shapes
VMCAI 2013: International Conference on Verification, Model Checking, and Abstract Interpretation