2015
Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages
ESOP 2015:
European Symposium on Programming
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
2014
16
2
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
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