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
2013
A Bit Too Precise? Verification of Quantized Digital Filters
2013-6
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
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
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