2023
Historia: Refuting Callback Reachability with Message-History Logics
OOPSLA 2023:
ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications
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
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
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
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
Huisong Li, Bor-Yuh Evan Chang, and Xavier Rival
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
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
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
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
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
Bor-Yuh Evan Chang, Matthew Harren, and George C. Necula
SAS 2006:
International Static Analysis Symposium
Extended Version:
Technical Report
(UCB/EECS-2006-86)
2005
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
Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, and Frank Pfenning
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