2024
Interactive Abstract Interpretation with Demanded Summarization
ACM Transactions on Programming Languages and Systems (TOPLAS) ACM Trans. Program. Lang. Syst.
2023
Historia: Refuting Callback Reachability with Message-History Logics
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
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
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.
2019
Static Analysis with Demand-Driven Value Refinement
Proceedings of the ACM on Programming Languages PACMPL
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
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
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
2016
A Vision for Online Verification-Validation
GPCE 2016: ACM SIGPLAN International Conference on Generative Programming and Component Engineering
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
Shape Analysis for Unstructured Sharing
SAS 2015: International Static Analysis Symposium
2015
Droidel: A General Approach to Android Framework Modeling
SOAP 2015: ACM SIGPLAN Workshop on State of the Art in Program Analysis
2015
Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages
ESOP 2015: European Symposium on Programming
2015
In Defense of Soundiness: A Manifesto
Communications of the ACM (CACM) Commun. ACM
2014
Construction of Abstract Domains for Heterogeneous Properties (Position Paper)
ISOLA 2014: International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
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
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
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
QUIC Graphs: Relational Invariant Generation for Containers
ECOOP 2013: European Conference on Object-Oriented Programming
2013
Thresher: Precise Refutations for Heap Reachability
PLDI 2013: ACM SIGPLAN Conference on Programming Language Design and Implementation
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
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
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
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
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
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
2017
Abstracting Event-Driven Systems with Lifestate Rules
Technical Report (arXiv:1701.00161)
2015
Synthesizing Short-Circuiting Validation of Data Structure Invariants
Technical Report (arXiv:1511.04846)
2008
End-User Program Analysis
Ph.D. Dissertation
Also available as Technical Report (UCB/EECS-2008-161)
2008
Relational Inductive Shape Analysis
POPL 2008: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
2007
Shape Analysis with Structural Invariant Checkers
SAS 2007: International Static Analysis Symposium
Extended Version: Technical Report (UCB/EECS-2007-80)
2006
Analysis of Low-Level Code Using Cooperating Decompilers
SAS 2006: International Static Analysis Symposium
Extended Version: Technical Report (UCB/EECS-2006-86)
2005
Boogie: A Modular Reusable Verifier for Object-Oriented Programs
FMCO 2005: International Symposium on Formal Methods for Components and Objects
2006
A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety
VMCAI 2006: International Conference on Verification, Model Checking, and Abstract Interpretation
Extended Version: Technical Report (UCB/ERL M05/32)
2005
Type-Based Verification of Assembly Language
M.S. Thesis
Also available as Technical Report (UCB/EECS-2008-186)
2005
Abstract Interpretation with Alien Expressions and Heap Structures
VMCAI 2005: International Conference on Verification, Model Checking, and Abstract Interpretation
Extended Version: Technical Report (MSR-TR-2004-115)
2005
Inferring Object Invariants
AIOOL 2005: International Workshop on Abstract Interpretation of Object-Oriented Languages
2005
Type-Based Verification of Assembly Language for Compiler Debugging
TLDI 2005: ACM SIGPLAN International Workshop on Types in Language Design and Implementation
2005
The Open Verifier Framework for Foundational Verifiers
TLDI 2005: ACM SIGPLAN International Workshop on Types in Language Design and Implementation
2003
PML: Toward a High-Level Formal Language for Biological Systems
BioConcur 2003: Workshop on Concurrent Models in Molecular Biology
Extended Version: Technical Report (UCB/CSD-03-1251)
2003
A Judgmental Analysis of Linear Logic
Technical Report CMU-CS-03-131R
2002
Trustless Grid Computing in ConCert
GRID 2002: International Workshop on Grid Computing
2002
Iktara in ConCert: Realizing a Certified Grid Computing Framework from a Programmer's Perspective
Senior Thesis
Also available as Technical Report (CMU-CS-02-150)
2001
Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic
PTP 2001: Workshop on Proof Transformations, Proof Presentations, and Complexity of Proofs