Faculty

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

Post-Docs

Mohamed Amin Ben Sassi
Yuen-Lam Voronin

Students

PhD

Sam Blackshear
Aleksandar Chakarov
Alexandra Gendreau
Youngsung Kim
Jedidiah McClurg
Shawn Meier
Hadi Ravanbakhsh
Aditya Zutshi

BS/BA+MS

Ross Holland

BS/BA

Kyle Howell
Evan Roncevich
Max Russek

Alumni

Faculty

Amer Diwan
Jeremy G. Siek

PhD

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

BS/BA+MS

Kira Quan
Erik Silkensen

MS

Neelam Agrawal
Huck Bennett
Shashank Bharadwaj
Yi-Fan Tsai
Jonathan Turner

BS/BA

Alex Beal
Nicholas Vanderweit
Paul Givens

Affiliates

2015.06.01:
CUPLV author Bor-Yuh Evan Chang with collaborators has had a paper "Shape Analysis for Unstructured Sharing" accepted for presentation at SAS 2015 in September.
2015.05.27:
Mayur Naik from Georgia Tech is visiting us on May 28-29, 2015. He is giving a CUPLV Seminar entitled "Petablox: Declarative Program Analysis for Big Code" at 10:30am in DLC 1B70 on Friday, May 29, 2015.
2015.05.27:
Sam Blackshear is defending his PhD on at 1:00pm in ECAE 199 on Thursday, May 28, 2015. His PhD is entitled "Flexible Goal-Directed Abstraction."
2015.05.18:
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.04.26:
Matthew A. Hammer joins CUPLV as an assistant professor of computer science in Fall 2015. Welcome, Matt!
2015.04.25:
CUPLV author Pavol Černý has had papers accepted for presentation at CAV 2015 in July (Alur et al. and Černý et al.).
2015.04.25:
CUPLV authors Sam Blackshear, Alexandra Gendreau, and Bor-Yuh Evan Chang have had a paper "Droidel: A General Approach to Android Framework Modeling" accepted for presentation at SOAP 2015 in June.
2015.04.21:
CUPLV faculty Pavol Černý, Bor-Yuh Evan Chang, Sriram Sankaranarayanan have been awarded a DARPA grant "STAC: Auditr: Securing Space/Time Defenses in Java Bytecode" with collaborators John Black at CU, Işıl Dillig and Marijn J. H. Heule at UT Austin, and Henny Sipma at Kestrel Technology.
2015.04.21:
CUPLV authors Youngsung Kim and Pavol Černý with collaborators have had a paper "Performance Search Engine Driven by Prior Knowledge of Optimization" accepted for presentation at ARRAY 2015 in June.
2015.04.16:
Ashutosh Trivedi from IIT Bombay is visiting us on April 17, 2015. He is giving a CUPLV Seminar entitled "Decidable Subclasses of Multi-Mode Systems" at 1:00pm in KOBL 235 on Friday, April 17, 2015.
2015.02.16:
Prospective Ph.D. students visit February 20. Welcome!
2015.02.11:
CUPLV authors Jedidiah McClurg and Pavol Černý and collaborators at Cornell have had a paper accepted for presentation at PLDI 2015 in June (McClurg et al.).
2014.12.16:
CUPLV authors Arlen Cox, Bor-Yuh Evan Chang, and Pavol Černý with collaborators have had papers accepted for presentation at ESOP 2015 in April (Cox et al. and Černý et al.).
2014.11.30:
Leonid Ryzhyk from Carnegie Mellon University is visiting us on December 5, 2014. He is giving a CUPLV Seminar entitled "Automatic Device Driver Synthesis" at 4:00pm in ECOT 831 on Friday, December 5, 2014.
2014.11.30:
Manu Sridharan from Samsung Research America is visiting us on December 3, 2014. He is giving a CUPLV Seminar entitled "MemInsight: Platform-Independent Memory Profiling for JavaScript" at 4:00pm in ECCR 116 on Wednesday, December 3, 2014.
2015.06.01: Paper by Li et al. accepted to SAS 2015.
2015.05.27: Mayur Naik visits May 28-29.
2015.05.27: Sam Blackshear defends his PhD on May 28.
2015.05.18: Call for postdoc applicants for Summer or Fall 2015.
2015.04.26: Matthew A. Hammer is joining CUPLV!
2015.04.25: Two papers with CUPLV authors accepted to CAV 2015! [1, 2]
2015.04.25: Paper by Blackshear et al. accepted to SOAP 2015.
2015.04.21: Paper by Kim et al. accepted to ARRAY 2015.
2015.04.16: Ashutosh Trivedi visits April 17.
2015.02.16: Prospective Ph.D. students visit February 20. Welcome!
2015.02.11: McClurg et al. paper accepted to PLDI 2015!
2014.12.16: Two papers with CUPLV authors accepted to ESOP 2015! [1, 2]
2014.11.30: Leonid Ryzhyk visits December 5.
2014.11.30: Manu Sridharan visits December 3.
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

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

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

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

ISOLA 2014Imperial, Corfu, GreeceOctober 2014

2014
Construction of Abstract Domains for Heterogeneous Properties (Position Paper)
ISOLA 2014: International Symposium on Leveraging Applications of Formal Methods, Verification and Validation

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