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
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

Affiliates

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!
2013.10.01:
CUPLV authors Devin Coughlin, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan with collaborators have had papers accepted for presentation at POPL 2014 in January (Coughlin and Chang and Jeannet et al.).
2013.06.08:
Eight CUPLV papers are being presented this summer: PLDI 2013 June 16-22 [Blackshear et al., Sankaranarayanan et al., Blackshear and Lahiri], LICS 2013 June 25-28 [Chaudhuri et al.], ECOOP 2013 July 1-5 [Cox et al.], and CAV 2013 July 13-19 [Černý et al., Chakarov and Sankaranarayanan, Chen et al.].
2013.05.21:
Arlen Cox wins a Chateaubriand Fellowship in Science, Technology, Engineering, and Mathematics from the Embassy of France in the United States to study and conduct research in France.
2013.05.07:
The artifact supplementing "QUIC Graphs: Relational Invariant Generation for Containers" has been validated and has received the distinguished artifact award at ECOOP 2013!
2013.03.06:
CUPLV authors Pavol Černý, Aleksandar Chakarov, and Sriram Sankaranarayanan with collaborators have had papers accepted for presentation at CAV 2013 in July (Černý et al., Chakarov and Sankaranarayanan, and Chen et al.).
2012.03.04:
CUPLV authors Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan have had a paper "QUIC Graphs: Relational Invariant Generation for Containers" accepted for presentation at ECOOP 2013 in July.
2013.03.04:
Submit Analyzer Pearls to TAPAS 2013!
2013.02.21:
Prospective Ph.D. students visit February 22. Welcome!
2013.02.04:
CUPLV authors Sam Blackshear, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Aleksandar Chakarov with collaborators Manu Sridharan, Sumit Gulwani, and Shuvendu Lahiri have had papers accepted for presentation at PLDI 2013 in June (Blackshear et al., Sankaranarayanan et al., and Blackshear and Lahiri).
2013.01.31:
Nathan Lapinksi and Sriram Sankaranarayanan have had their poster accepted to the SIGCSE 2013 Student Research Competition.
2013.01.31:
Paul Givens, Aleksandar Chakarov, Sriram Sankaranarayanan, and Tom Yeh have had their paper accepted for presentation at ICSE 2013 (New and Emerging Results Track) in May.
2013.01.23:
Sumit K. Jha from University of Central Florida is visiting us on January 24, 2013. He is giving a Computer Science Colloquium entitled "Validation and Parameter Discovery for Stochastic Computational Models from Behavioral Specifications" at 3:30pm in ECCR 265 on Thursday, January 24, 2013.
2014.02.19: Prospective Ph.D. students visit February 21. Welcome!
2013.10.01: Two papers with CUPLV authors accepted to POPL 2014! [1, 2]
2013.06.08: Check out CUPLV at PLDI 2013, LICS 2013, ECOOP 2013, and CAV 2013 this summer.
2013.05.21: Arlen Cox wins a Chateaubriand Fellowship!
2013.05.07: Cox et al. wins ECOOP 2013 distinguished artifact award!
2013.03.06: Three papers with CUPLV authors accepted to CAV 2013! [1, 2, 3]
2012.03.04: Paper by Cox et al. accepted to ECOOP 2013.
2013.03.04: Submit Analyzer Pearls to TAPAS 2013!
2013.02.21: Prospective Ph.D. students visit February 22. Welcome!
2013.02.04: Great showing for CUPLV authors at PLDI 2013: 3 papers accepted! [1, 2, 3]
2013.01.31: Poster accepted to SIGCSE 2013 Student Research Competition (by Nathan Lapinksi et al.).
2013.01.31: Paper accepted to ICSE 2013 (New and Emerging Results Track) (by Givens et al.).
2013.01.23: Sumit K. Jha visits January 24.
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, 2013.

Projects

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

Recent Publications

PLDI 2014Edinburgh, UKJune 2014

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

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