Faculty

Pavol Černý
Bor-Yuh Evan Chang
Dirk Grunwald
Matthew A. Hammer
Sriram Sankaranarayanan
Fabio Somenzi
Ashutosh Trivedi

Scientists

Post-Docs

Xin Chen
Sergio Mover
Yuen-Lam Voronin

Students

PhD

Aleksandar Chakarov
Michael Dooley
Kyle Headley
Youngsung Kim
Tianhan Lu
Jedidiah McClurg
Shawn Meier
Saeid Tizpaz Niari
Hadi Ravanbakhsh
Benno Stein
Aditya Zutshi

MS

Yi Chou
Ram Das Diwakaran
Dimitrios Economou
Nilesh Jagnik
Suhas Akshar Kumar
Aniket Kumar Lata
Anna Villani

BS/BA

Dakota Fisher
Jay Lecavlier
Alexandra Okeson
Rhys Braginton Pettee Olsen
Max Russek

Graduate Interns

Théotime Grohens

Alumni

Faculty

Amer Diwan
Jeremy G. Siek

Post-Docs

Mohamed Amin Ben Sassi

PhD

Geoffrey Belter
Sam Blackshear
Devin Coughlin
Arlen Cox
Justin E. Gottschlich
Ian Karlin
Weiyu Miao
Todd Mytkowicz
Christoph Reichenbach
Yan Zhang

BS/BA+MS

Ross Holland
Kyle Howell
Kira Quan
Erik Silkensen

MS

Neelam Agrawal
Huck Bennett
Shashank Bharadwaj
Vaibhav Singh
Krishna Chaitanya Sripada
Yi-Fan Tsai
Jonathan Turner

BS/BA

Alex Beal
Parker Evans
Paul Givens
Nathan Lapinksi
Evan Roncevich
Nicholas Vanderweit

Visiting Scholars

Pierre Roux

Affiliates

2015.06.17:
Congratulations to Benno Stein for being awarded second place in the graduate student category at the PLDI Student Research Competition (SRC) for his project, "Goal-Directed Abstract Interpretation for JavaScript."
2016.06.14:
CUPLV authors Pierre Roux, Yuen-Lam Voronin, and Sriram Sankaranarayanan have had a paper "Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants" accepted for presentation at SAS 2016 in September.
2016.05.20:
CUPLV authors Hadi Ravanbakhsh and Sriram Sankaranarayanan have had a paper "Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework" accepted for presentation at EMSOFT 2016 in October.
2016.05.13:
CUPLV faculty Matthew A. Hammer and Bor-Yuh Evan Chang have been awarded an NSF grant "Online Verification-Validation" with collaborator David Van Horn at the University of Maryland.
2016.05.06:
CUPLV authors Michael Dooley, Fabio Somenzi, and Sergio Mover have had papers accepted for presentation at CAV 2016 in July (Dooley and Somenzi and Daniel et al.).
2016.04.19:
Saeid Tizpaz Niari wins Second Prize in the Microsoft Open Source Challenge for his entry "CONfidentiality CERTifier: a Modeling and Verification Framework for Program Confidentiality using Z3".
2016.04.17:
CUPLV authors Jedidiah McClurg and Pavol Černý and collaborators at Cornell have had a paper accepted for presentation at PLDI 2016 in June (McClurg et al.).
2016.04.13:
Aditya Zutshi wins the Best Student Paper Award at HSCC 2016 for his paper "Symbolic-Numeric Reachability Analysis of Closed-Loop Control Software" co-authored with Sriram Sankaranarayanan and collaborators.
2015.12.20:
CUPLV authors Aditya Zutshi, Sriram Sankaranarayanan, and with collaborators have had a paper "Symbolic-Numeric Reachability Analysis of Closed-Loop Control Software" accepted for presentation at HSCC 2016 in April.
2015.12.18:
CUPLV authors Aleksandar Chakarov, Yuen-Lam Voronin, and Sriram Sankaranarayanan with collaborators have had papers accepted for presentation at TACAS 2016 in April (Bouissou et al. and Chakarov et al.).
2015.11.01:
Please consider applying or encourage your students and postdocs to apply for a tenure-track position in the Department of Computer Science (CS) and Department of Electrical, Computer, and Energy Engineering (ECEE) at the University of Colorado Boulder. We have multiple openings with one particular interest area in Computer Science being secure and reliable software systems. Applications will be evaluated beginning on November 9, 2015 with priority given to applications received by December 7, 2015, although applications will continue to be evaluated until the position is filled. Apply at http://www.jobsatcu.com/postings/109940 for CS and at https://www.jobsatcu.com/postings/107808 for ECEE.
2015.11.01:
There is a postdoctoral research associate position open with the opportunity to work with Profs. Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Pavol Černý on program analysis and program synthesis.
2015.11.01:
Call for Ph.D. applicants for Fall 2016. Application deadline is December 15, 2015. Check out our latest recruiting talk from February 20, 2015.
2015.10.15:
Thomas Ball from Microsoft Research is visiting us on October 19-20, 2015. He is giving a CUPLV Seminar entitled "Recent Results in Automated Verification from Microsoft Research" at 9:30am in ECCR 150 on Tuesday, October 20, 2015.
2015.08.04:
CUPLV authors Sam Blackshear, Bor-Yuh Evan Chang, Matthew A. Hammer, and Kyle Headley have had papers accepted for presentation at OOPSLA 2015 in October (Blackshear et al. and Hammer et al.).
2015.06.17: Benno Stein awarded second place at the PLDI Student Research Competition (SRC).
2016.06.14: Paper by Roux et al. accepted to SAS 2016.
2016.05.20: Paper by Ravanbakhsh and Sankaranarayanan accepted to EMSOFT 2016.
2016.05.06: Two papers with CUPLV authors accepted to CAV 2016! [1, 2]
2016.04.19: Saeid Tizpaz Niari wins Second Prize in the Microsoft Open Source Challenge.
2016.04.17: McClurg et al. paper accepted to PLDI 2016!
2016.04.13: Aditya Zutshi wins the Best Student Paper Award at HSCC 2016.
2015.12.20: Paper by Zutshi et al. accepted to HSCC 2016.
2015.12.18: Two papers with CUPLV authors accepted to TACAS 2016! [1, 2]
2015.11.01: Multiple tenure-track openings in CS and ECEE.
2015.11.01: Call for postdoc applicants for Spring or Summer 2016.
2015.11.01: Call for Ph.D. applicants for Fall 2016. Application deadline is December 15, 2015.
2015.10.15: Thomas Ball visits October 19-20.
2015.08.04: Two papers with CUPLV authors accepted to OOPSLA 2015! [1, 2]
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, 2015.
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

DroidelA Framework Model for Static Analysis of Android Applications
QUIC GraphsRelational Invariant Generation for Containers
ThresherPrecise Refutations for Heap Reachability
Fissile Type AnalysisModular Checking of Almost-Everywhere Invariants

Recent Publications

EMSOFT 2016Pittsburgh, Pennsylvania, USAOctober 2016

2016
Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework
Hadi Ravanbakhsh and Sriram Sankaranarayanan
EMSOFT 2016: ACM SIGBED International Conference on Embedded Software

SAS 2016Edinburgh, UKSeptember 2016

2016
Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants
SAS 2016: International Static Analysis Symposium

CAV 2016Toronto, Ontario, CanadaJuly 2016

2016
Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances
Michael Dooley and Fabio Somenzi
CAV 2016: International Conference on Computer Aided Verification
2016
Infinite-state Liveness-to-Safety via Implicit Abstraction and Well-founded Relations
CAV 2016: International Conference on Computer Aided Verification

PLDI 2016Santa Barbara, California, USAJune 2016

2016
Event-Driven Network Programming
PLDI 2016: ACM SIGPLAN Conference on Programming Language Design and Implementation

HSCC 2016Vienna, AustriaApril 2016

2016
Symbolic-Numeric Reachability Analysis of Closed-Loop Control Software
Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy V. Deshmukh, and Xiaoqing Jin
HSCC 2016: International Conference on Hybrid Systems: Computation and Control

TACAS 2016Eindhoven, The NetherlandsApril 2016

2016
Uncertainty Propagation using Probabilistic Affine Forms and Concentration of Measure Inequalities
Olivier Bouissou, Eric Goubault, Sylvie Putot, Aleksandar Chakarov, and Sriram Sankaranarayanan
TACAS 2016: International Conference on Tools and Algorithms for the Construction and Analysis of Systems
2016
Deductive Proofs of Almost Sure Persistence and Recurrence Properties
Aleksandar Chakarov, Yuen-Lam Voronin, and Sriram Sankaranarayanan
TACAS 2016: International Conference on Tools and Algorithms for the Construction and Analysis of Systems

LPAR 2015Suva, FijiNovember 2015

2015
Abstract Domains and Solvers for Sets Reasoning
LPAR 2015: International Conference on Logic for Programming, Artificial Intelligence and Reasoning

OOPSLA 2015Pittsburgh, Pennsylvania, USAOctober 2015

2015
Selective Control-Flow Abstraction via Jumping
OOPSLA 2015: ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications
2015
Incremental Computation with Names
OOPSLA 2015: ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications

SAS 2015Saint-Malo, FranceSeptember 2015

2015
Shape Analysis for Unstructured Sharing
SAS 2015: International Static Analysis Symposium

CAV 2015San Francisco, California, USAJuly 2015

2015
Synthesis through Unification
CAV 2015: International Conference on Computer Aided Verification
2015
From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis
CAV 2015: International Conference on Computer Aided Verification

SOAP 2015Portland, Oregon, USAJune 2015

2015
Droidel: A General Approach to Android Framework Modeling
SOAP 2015: ACM SIGPLAN Workshop on State of the Art in Program Analysis

ARRAY 2015Portland, Oregon, USAJune 2015

2015
Performance Search Engine Driven by Prior Knowledge of Optimization
Youngsung Kim, Pavol Černý, and John Dennis
ARRAY 2015: ACM SIGPLAN Workshop on Libraries, Languages and Compilers for Array Programming

PLDI 2015Portland, Oregon, USAJune 2015

2015
Efficient Synthesis of Network Updates
PLDI 2015: ACM SIGPLAN Conference on Programming Language Design and Implementation

ESOP 2015London, United KingdomApril 2015

2015
Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages
ESOP 2015: European Symposium on Programming
2015
Segment Abstraction for Worst-Case Execution Time Analysis
ESOP 2015: European Symposium on Programming