2024
Interactive Abstract Interpretation with Demanded Summarization
Benno Stein, Bor-Yuh Evan Chang, and Manu Sridharan
ACM Transactions on Programming Languages and Systems (TOPLAS) ACM Trans. Program. Lang. Syst.
2023
Historia: Refuting Callback Reachability with Message-History Logics
Shawn Meier, Sergio Mover, Gowtham Kaki, and Bor-Yuh Evan Chang
OOPSLA 2023: ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications
2023
Verifying Indistinguishability of Privacy-Preserving Protocols
Kirby Linvill, Gowtham Kaki, and Eric Wustrow
Proceedings of the ACM on Programming Languages PACMPL
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
Tianhan Lu, Bor-Yuh Evan Chang, and Ashutosh Trivedi
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
Benno Stein, Bor-Yuh Evan Chang, and Manu Sridharan
PLDI 2021: ACM SIGPLAN Conference on Programming Language Design and Implementation
2020
Shape Analysis
Bor-Yuh Evan Chang, Cezara Drăgoi, Roman Manevich, Noam Rinetzky, and Xavier Rival
Foundations and Trends in Programming Languages (FnTPL) Found. Trends Program. Lang.
2020
Reachability Analysis using Message Passing over Tree Decompositions
Sriram Sankaranarayanan
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
Benno Stein, Benjamin Barslev Nielsen, Bor-Yuh Evan Chang, and Anders Møller
Proceedings of the ACM on Programming Languages PACMPL
2019
Efficient Detection and Quantification of Timing Leaks with Neural Networks
Saeid Tizpaz Niari, Pavol Černý, Sriram Sankaranarayanan, and Ashutosh Trivedi
RV 2019: International Conference on Runtime Verification
2019
Predictive Runtime Monitoring for Linear Stochastic Systems and Applications to Geofence Enforcement for UAVs
Hansol Yoon, Chou Yi, Xin Chen, Eric Frew, and Sriram Sankaranarayanan
RV 2019: International Conference on Runtime Verification
2019
Robustness of Specifications and its Applications to Falsification, Parameter Mining, and Runtime Monitoring with S-TaLiRo
Georgios Fainekos, Bardh Hoxha, and Sriram Sankaranarayanan
RV 2019: International Conference on Runtime Verification
2019
Sequential Programming for Replicated Data Stores
Nicholas V. Lewchenko, Arjun Radhakrishna, Akash Gaonkar, and Pavol Černý
ICFP 2019: ACM SIGPLAN International Conference on Functional Programming
2019
Quantitative Mitigation of Timing Side Channels
Saeid Tizpaz Niari, Pavol Černý, and Ashutosh Trivedi
CAV 2019: International Conference on Computer Aided Verification
2019
Lifestate: Event-Driven Protocols and Callback Control Flow
Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang
ECOOP 2019: European Conference on Object-Oriented Programming
2019
Type-directed Bounding of Collections in Reactive Programs
Tianhan Lu, Pavol Černý, Bor-Yuh Evan Chang, and Ashutosh Trivedi
VMCAI 2019: International Conference on Verification, Model Checking, and Abstract Interpretation
2018
Safe Stream-Based Programming with Refinement Types
Benno Stein, Lazaro Clapp, Manu Sridharan, and Bor-Yuh Evan Chang
ASE 2018: IEEE/ACM International Conference on Automated Software Engineering
2018
Robust Data-Driven Control of Artificial Pancreas Systems using Neural Networks
Souradeep Dutta, Taisa Kushner, and Sriram Sankaranarayanan
CMSB 2018: International Conference on Computational Methods in Systems Biology
2018
Almost-Sure Reachability in Stochastic Multi-Mode System
Fabio Somenzi, Behrouz Touri, and Ashutosh Trivedi
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
Arjun Radhakrishna, Nicholas V. Lewchenko, Shawn Meier, Sergio Mover, Bor-Yuh Evan Chang, and Pavol Černý
ICSE 2018: International Conference on Software Engineering
2018
Differential Performance Debugging with Discriminant Regression Trees
Saeid Tizpaz Niari, Pavol Černý, Bor-Yuh Evan Chang, and Ashutosh Trivedi
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
Xin Chen, Sergio Mover, and Sriram Sankaranarayanan
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
Saeid Tizpaz Niari, Pavol Černý, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Ashutosh Trivedi
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
Matthew A. Hammer, Bor-Yuh Evan Chang, and David Van Horn
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
Pierre Roux, Yuen-Lam Voronin, and Sriram Sankaranarayanan
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
Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, and Sergio Mover
CAV 2016: International Conference on Computer Aided Verification
2016
Event-Driven Network Programming
Jedidiah McClurg, Hossein Hojjat, Nate Foster, and Pavol Černý
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
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
2015
Abstract Domains and Solvers for Sets Reasoning
Arlen Cox, Bor-Yuh Evan Chang, Huisong Li, and Xavier Rival
LPAR 2015: International Conference on Logic for Programming, Artificial Intelligence and Reasoning
2015
Selective Control-Flow Abstraction via Jumping
Sam Blackshear, Bor-Yuh Evan Chang, and Manu Sridharan
OOPSLA 2015: ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications
2015
Incremental Computation with Names
Matthew A. Hammer, Joshua Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael Hicks, and David Van Horn
OOPSLA 2015: ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications
2015
Shape Analysis for Unstructured Sharing
Huisong Li, Bor-Yuh Evan Chang, and Xavier Rival
SAS 2015: International Static Analysis Symposium
2015
Synthesis through Unification
Rajeev Alur, Pavol Černý, and Arjun Radhakrishna
CAV 2015: International Conference on Computer Aided Verification
2015
From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis
Pavol Černý, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach
CAV 2015: International Conference on Computer Aided Verification
2015
Droidel: A General Approach to Android Framework Modeling
Sam Blackshear, Alexandra Gendreau, and Bor-Yuh Evan Chang
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
Jedidiah McClurg, Hossein Hojjat, Pavol Černý, and Nate Foster
PLDI 2015: ACM SIGPLAN Conference on Programming Language Design and Implementation
2015
Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages
Arlen Cox, Bor-Yuh Evan Chang, and Xavier Rival
ESOP 2015: European Symposium on Programming
2015
Segment Abstraction for Worst-Case Execution Time Analysis
Pavol Černý, Thomas A. Henzinger, Laura Kovács, Arjun Radhakrishna, and Jakob Zwirchmayr
ESOP 2015: European Symposium on Programming
2015
In Defense of Soundiness: A Manifesto
Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondřej Lhoták, J. Nelson Amaral, Bor-Yuh Evan Chang, Samuel Z. Guyer, Uday P. Khedker, Anders Møller, and Dimitrios Vardoulakis
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)
Xavier Rival, Antoine Toubhans, and Bor-Yuh Evan Chang
ISOLA 2014: International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
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
Arlen Cox, Bor-Yuh Evan Chang, and Xavier Rival
SAS 2014: International Static Analysis Symposium
2014
An Abstract Domain Combinator for Separately Conjoining Memory Abstractions
Antoine Toubhans, Bor-Yuh Evan Chang, and Xavier Rival
SAS 2014: International Static Analysis Symposium
2014
QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan
CAV 2014: International Conference on Computer Aided Verification
2014
Verification Modulo Versions: Towards Usable Verification
Francesco Logozzo, Manuel Fähndrich, Shuvendu Lahiri, and Sam Blackshear
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
Devin Coughlin and Bor-Yuh Evan Chang
POPL 2014: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2014
Abstract Acceleration of General Linear Loops
Bertrand Jeannet, Peter Schrammel, and Sriram Sankaranarayanan
POPL 2014: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2014
Refuting Heap Rechability (Extended Abstract)
Bor-Yuh Evan Chang
VMCAI 2014: International Conference on Verification, Model Checking, and Abstract Interpretation
2013
Modular Construction of Shape-Numeric Analyzers
Bor-Yuh Evan Chang and Xavier Rival
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
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
2013
QUIC Graphs: Relational Invariant Generation for Containers
Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan
ECOOP 2013: European Conference on Object-Oriented Programming
2013
Regular Real Analysis
Swarat Chaudhuri, Sriram Sankaranarayanan, and Moshe Vardi
LICS 2013: IEEE Symposium on Logic in Computer Science
2013
Thresher: Precise Refutations for Heap Reachability
Sam Blackshear, Bor-Yuh Evan Chang, and Manu Sridharan
PLDI 2013: ACM SIGPLAN Conference on Programming Language Design and Implementation
2013
Almost-Correct Specifications: A Modular Semantic Framework for Assigning Confidence to Warnings
Sam Blackshear and Shuvendu Lahiri
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
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
2014
A Bit Too Precise? Verification of Quantized Digital Filters
Arlen Cox, Sriram Sankaranarayanan, and Bor-Yuh Evan Chang
International Journal on Software Tools for Technology Transfer (STTT) Int J Softw Tools Technol Transfer
2013
Quantitative Abstraction Refinement
Pavol Černý, Thomas A. Henzinger, and Arjun Radhakrishna
POPL 2013: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2013
Reduced Product Combination of Abstract Domains for Shapes
Antoine Toubhans, Bor-Yuh Evan Chang, and Xavier Rival
VMCAI 2013: International Conference on Verification, Model Checking, and Abstract Interpretation
2012
Invariant Generation for Parametrized Systems using Self-Reflection
Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez, and Bor-Yuh Evan Chang
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
Devin Coughlin, Bor-Yuh Evan Chang, Amer Diwan, and Jeremy G. Siek
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
Josh Berdine, Arlen Cox, Samin Ishtiaq, and Christoph Wintersteiger
CAV 2012: International Conference on Computer Aided Verification
2012
Timed Relational Abstractions of Sampled-Data Control Systems
Aditya Zutshi, Sriram Sankaranarayanan, and Ashish Tiwari
CAV 2012: International Conference on Computer Aided Verification
2012
Incremental Inductive CTL Model Checking
Zyad Hassan, Aaron R. Bradley, and Fabio Somenzi
CAV 2012: International Conference on Computer Aided Verification
2012
A Bit Too Precise? Bounded Verification of Quantized Digital Filters
Arlen Cox, Sriram Sankaranarayanan, and Bor-Yuh Evan Chang
TACAS 2012: International Conference on Tools and Algorithms for the Construction and Analysis of Systems
2011
An Incremental Approach to Model Checking Progress Properties
Aaron R. Bradley, Fabio Somenzi, Zyad Hassan, and Yan Zhang
FMCAD 2011: International Conference on Formal Methods in Computer Aided Design
2011
The Flow-Insensitive Precision of Andersen's Analysis in Practice
Sam Blackshear, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Manu Sridharan
SAS 2011: International Static Analysis Symposium
Extended Version: Technical Report (CU-CS-1083-11)
2011
Relational Abstractions for Continuous and Hybrid Systems
Sriram Sankaranarayanan and Ashish Tiwari
CAV 2011: International Conference on Computer Aided Verification
2011
Automatic Abstraction of Non-Linear Systems Using Change of Variables Transformations
Sriram Sankaranarayanan
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
Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler
POPL 2011: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2011
Calling Context Abstraction with Shapes
Xavier Rival and Bor-Yuh Evan Chang
POPL 2011: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2011
Access Nets: Modeling Access to Physical Spaces
Robert Frohardt, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan
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
Khoo Yit Phang, Bor-Yuh Evan Chang, and Jeffrey S. Foster
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
Todd Mytkowicz, Amer Diwan, Matthias Hauswirth, and Peter F. Sweeney
PLDI 2010: ACM SIGPLAN Conference on Programming Language Design and Implementation
2010
Threesomes, With and Without Blame
Jeremy G. Siek and Philip Wadler
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)
Bor-Yuh Evan Chang, Amer Diwan, and Jeremy G. Siek
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