2023
Historia: Refuting Callback Reachability with Message-History Logics
OOPSLA 2023: ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications
2023
Verifying Indistinguishability of Privacy-Preserving Protocols
OOPSLA 2023: ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications
2023
Lifting On-Demand Analysis to Higher-Order Languages
Daniel Schoepe, David Seekatz, Ilina Stoilkovska, Sandro Stucki, Daniel Tattersall, Pauline Bolignano, Franco Raimondi, and Bor-Yuh Evan Chang
SAS 2023: International Static Analysis Symposium
2022
RunTime-assisted convergence in replicated data types
Gowtham Kaki, Prasanth Prahladan, and Nicholas V. Lewchenko
PLDI 2022: ACM SIGPLAN Conference on Programming Language Design and Implementation
2022
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
Ðorđe Žikelić, Bor-Yuh Evan Chang, Pauline Bolignano, and Franco Raimondi
PLDI 2022: ACM SIGPLAN Conference on Programming Language Design and Implementation
2021
Selectively-Amortized Resource Bounding
SAS 2021: International Static Analysis Symposium
2021
Model-Free Reinforcement Learning for Branching Markov Decision Processes.
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak
CAV 2021: International Conference on Computer Aided Verification
2021
Demanded Abstract Interpretation
PLDI 2021: ACM SIGPLAN Conference on Programming Language Design and Implementation
2020
Shape Analysis
Foundations and Trends in Programming Languages (FnTPL) Found. Trends Program. Lang.
2020
Reachability Analysis using Message Passing over Tree Decompositions
CAV 2020: International Conference on Computer Aided Verification
2020
Unbounded-Time Safety Verification of Stochastic Differential Dynamics
Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, and Naijun Zhan
CAV 2020: International Conference on Computer Aided Verification
2020
PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems
Alex Devonport, Mahmoud Khaled, Murat Arcak, and Majid Zamani
CAV 2020: International Conference on Computer Aided Verification
2020
AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems
Abolfazi Lavaei, Mahmoud Khaled, Sadegh Soudjani, and Majid Zamani
CAV 2020: International Conference on Computer Aided Verification
2019
Static Analysis with Demand-Driven Value Refinement
Proceedings of the ACM on Programming Languages PACMPL
2019
Efficient Detection and Quantification of Timing Leaks with Neural Networks
RV 2019: International Conference on Runtime Verification
2019
Predictive Runtime Monitoring for Linear Stochastic Systems and Applications to Geofence Enforcement for UAVs
RV 2019: International Conference on Runtime Verification
2019
Robustness of Specifications and its Applications to Falsification, Parameter Mining, and Runtime Monitoring with S-TaLiRo
RV 2019: International Conference on Runtime Verification
2019
Sequential Programming for Replicated Data Stores
ICFP 2019: ACM SIGPLAN International Conference on Functional Programming
2019
Quantitative Mitigation of Timing Side Channels
CAV 2019: International Conference on Computer Aided Verification
2019
Lifestate: Event-Driven Protocols and Callback Control Flow
ECOOP 2019: European Conference on Object-Oriented Programming
2019
Type-directed Bounding of Collections in Reactive Programs
VMCAI 2019: International Conference on Verification, Model Checking, and Abstract Interpretation
2018
Safe Stream-Based Programming with Refinement Types
ASE 2018: IEEE/ACM International Conference on Automated Software Engineering
2018
Robust Data-Driven Control of Artificial Pancreas Systems using Neural Networks
CMSB 2018: International Conference on Computational Methods in Systems Biology
2018
Almost-Sure Reachability in Stochastic Multi-Mode System
HSCC 2018: International Conference on Hybrid Systems: Computation and Control
2018
A Data-Driven Approach to Artificial Pancreas Verification and Synthesis
Taisa Kushner, David Bortz, David Maahs, and Sriram Sankaranarayanan
ICCPS 2018: International Conference on Cyber-Physical Systems
2018
Mining Framework Usage Graphs from App Corpora
Sergio Mover, Sriram Sankaranarayanan, Rhys Braginton Pettee Olsen, and Bor-Yuh Evan Chang
SANER 2018: International Conference on Software Analysis, Evolution and Reengineering
2018
DroidStar: Callback Typestates for Android Classes
ICSE 2018: International Conference on Software Engineering
2018
Differential Performance Debugging with Discriminant Regression Trees
AAAI 2018: AAAI Conference on Artificial Intelligence
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
Compositional Relational Abstraction for Nonlinear Hybrid Systems
EMSOFT 2017: ACM SIGBED International Conference on Embedded 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