2017
ChimpCheck: Property-Based Randomized Test Generation for Interactive Apps
Edmund S.L. Lam, Peilun Zhang, and Bor-Yuh Evan Chang
ONWARD! 2017: ACM Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software
2017
Learning Lyapunov (Potential) Functions from Counterexamples and Demonstrations
Hadi Ravanbakhsh and Sriram Sankaranarayanan
RSS 2017: Robotics: Science and Systems
2017
Discriminating Traces with Time
TACAS 2017: International Conference on Tools and Algorithms for the Construction and Analysis of Systems
2017
Semantic-Directed Clumping of Disjunctive Abstract States
Huisong Li, François Bérenger, Bor-Yuh Evan Chang, and Xavier Rival
POPL 2017: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2017
Hazelnut: A Bidirectionally Typed Structure Editor Calculus
Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer
POPL 2017: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2016
A Vision for Online Verification-Validation
GPCE 2016: ACM SIGPLAN International Conference on Generative Programming and Component Engineering
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
2016
Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants
SAS 2016: International Static Analysis Symposium
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
2016
Event-Driven Network Programming
PLDI 2016: ACM SIGPLAN Conference on Programming Language Design and Implementation
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
2016
Uncertainty Propagation using Probabilistic Affine Forms and Concentration of Measure Inequalities
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
TACAS 2016: International Conference on Tools and Algorithms for the Construction and Analysis of Systems
2015
Abstract Domains and Solvers for Sets Reasoning
LPAR 2015: International Conference on Logic for Programming, Artificial Intelligence and Reasoning
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
2015
Shape Analysis for Unstructured Sharing
SAS 2015: International Static Analysis Symposium
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
2015
Droidel: A General Approach to Android Framework Modeling
SOAP 2015: ACM SIGPLAN Workshop on State of the Art in Program Analysis
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
2015
Efficient Synthesis of Network Updates
PLDI 2015: ACM SIGPLAN Conference on Programming Language Design and Implementation
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
2015
In Defense of Soundiness: A Manifesto
Communications of the ACM (CACM) Commun. ACM
2014
Infinite Horizon Safety Controller Synthesis through Disjunctive Polyhedral Abstract Interpretation
Hadi Ravanbakhsh and Sriram Sankaranarayanan
EMSOFT 2014: ACM SIGBED 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: ACM SIGBED International Conference on Embedded Software
2014
Construction of Abstract Domains for Heterogeneous Properties (Position Paper)
ISOLA 2014: International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
2014
Expectation Invariants for Probabilistic Program Loops as Fixed Points
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
2014
QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
CAV 2014: International Conference on Computer Aided Verification
2014
Verification Modulo Versions: Towards Usable Verification
PLDI 2014: ACM SIGPLAN Conference on Programming Language Design and Implementation
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
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
2014
Refuting Heap Rechability (Extended Abstract)
VMCAI 2014: International Conference on Verification, Model Checking, and Abstract Interpretation
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
2013
Efficient Synthesis for Concurrency using Semantics-Preserving Transformations
CAV 2013: International Conference on Computer Aided Verification
2013
Probabilistic Program Analysis with Martingales
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
2013
QUIC Graphs: Relational Invariant Generation for Containers
ECOOP 2013: European Conference on Object-Oriented Programming
2013
Regular Real Analysis
LICS 2013: IEEE Symposium on Logic in Computer Science
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
PLDI 2013: ACM SIGPLAN Conference on Programming Language Design and Implementation
2013
Exploring the Internal State of User Interfaces by Combining Computer Vision Techniques with Grammatical Inference
ICSE-NIER 2013: New and Emerging Results Track at ICSE
2014
A Bit Too Precise? Verification of Quantized Digital Filters
International Journal on Software Tools for Technology Transfer (STTT) Int J Softw Tools Technol Transfer
2013
Quantitative Abstraction Refinement
POPL 2013: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2013
Reduced Product Combination of Abstract Domains for Shapes
VMCAI 2013: International Conference on Verification, Model Checking, and Abstract Interpretation
2012
Invariant Generation for Parametrized Systems using Self-Reflection
SAS 2012: International Static Analysis Symposium
Extended Version: Technical Report (CU-CS-1094-12)
2012
Measuring Enforcement Windows with Symbolic Trace Interpretation: What Well-Behaved Programs Say
ISSTA 2012: International Symposium on Software Testing and Analysis
Extended Version: Technical Report (CU-CS-1093-12)
2012
Diagnosing Abstraction Failure in Separation Logic-based Analyses
CAV 2012: International Conference on Computer Aided Verification
2012
Timed Relational Abstractions of Sampled-Data Control Systems
CAV 2012: International Conference on Computer Aided Verification
2012
Incremental Inductive CTL Model Checking
CAV 2012: International Conference on Computer Aided Verification
2012
A Bit Too Precise? Bounded Verification of Quantized Digital Filters
TACAS 2012: International Conference on Tools and Algorithms for the Construction and Analysis of Systems
2011
An Incremental Approach to Model Checking Progress Properties
FMCAD 2011: International Conference on Formal Methods in Computer Aided Design
2011
The Flow-Insensitive Precision of Andersen's Analysis in Practice
SAS 2011: International Static Analysis Symposium
Extended Version: Technical Report (CU-CS-1083-11)
2011
Relational Abstractions for Continuous and Hybrid Systems
CAV 2011: International Conference on Computer Aided Verification
2011
Automatic Abstraction of Non-Linear Systems Using Change of Variables Transformations
HSCC 2011: International Conference on Hybrid Systems: Computation and Control
2011
S-Taliro: A Tool for Temporal Logic Falsification for Hybrid Systems
Yashwant Annapureddy, Che Liu, Georgios Fainekos, and Sriram Sankaranarayanan
TACAS 2011: International Conference on Tools and Algorithms for the Construction and Analysis of Systems
2011
Generalizing the Template Polyhedral Domain
Michael Colon and Sriram Sankaranarayanan
ESOP 2011: European Symposium on Programming
2011
Blame for All
POPL 2011: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2011
Calling Context Abstraction with Shapes
POPL 2011: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2011
Access Nets: Modeling Access to Physical Spaces
VMCAI 2011: International Conference on Verification, Model Checking, and Abstract Interpretation
Extended Version: Technical Report (CU-CS-1076-10)
2010
Mixing Type Checking and Symbolic Execution
PLDI 2010: ACM SIGPLAN Conference on Programming Language Design and Implementation
Extended Version: Technical Report (CS-TR-4954)
2010
Evaluating the Accuracy of Java Profilers
PLDI 2010: ACM SIGPLAN Conference on Programming Language Design and Implementation
2010
Threesomes, With and Without Blame
POPL 2010: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2010
Incremental Type-Checking for Type-Reflective Metaprograms
Weiyu Miao and Jeremy G. Siek
GPCE 2010: ACM SIGPLAN International Conference on Generative Programming and Component Engineering
2010
An Efficient Software Transactional Memory Using Commit-Time Invalidation
Justin E. Gottschlich, Manish Vachharajani, and Jeremy G. Siek
CGO 2010: International Symposium on Code Generation and Optimization
2010
Separating Shape Graphs
Vincent Laviron, Bor-Yuh Evan Chang, and Xavier Rival
ESOP 2010: European Symposium on Programming
2009
Gradual Programming: Bridging the Semantic Gap (Position Paper)
PLDI-FIT 2009: Fun Ideas and Thoughts at ACM SIGPLAN Conference on Programming Language Design and Implementation
2009
Automating the Generation of Composed Linear Algebra Kernels
Geoffrey Belter, E.R. Jessup, Ian Karlin, and Jeremy G. Siek
SC 2009: International Conference on High Performance Computing Networking, Storage and Analysis