Papers

Relational Inductive Shape Analysis (ps): Bor-Yuh Evan Chang and Xavier Rival (2008)
Thirty-Fifth Symposium on Principles of Programming Languages (POPL'08), ©ACM.
Shape Analysis with Structural Invariant Checkers (ps): Bor-Yuh Evan Chang, Xavier Rival, and George C. Necula (2007)
Fourteenth International Static Analysis Symposium (SAS'07), LNCS, ©Springer-Verlag.
Extended version available as Technical Report UCB/EECS-2007-80 (pdf).
Analysis of Low-Level Code Using Cooperating Decompilers (ps): Bor-Yuh Evan Chang, Matthew Harren, and George C. Necula (2006)
Thirteenth International Static Analysis Symposium (SAS'06), LNCS, ©Springer-Verlag.
Extended version available as Technical Report UCB/EECS-2006-86 (pdf).
Boogie: A Modular Reusable Verifier for Object-Oriented Programs (ps): Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino (2006)
Fourth International Symposium on Formal Methods for Components and Objects (FMCO'05), Post-Proceedings, LNCS, ©Springer-Verlag.
A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety (ps): Bor-Yuh Evan Chang, Adam Chlipala, and George C. Necula (2006)
Seventh International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'06), LNCS, ©Springer-Verlag.
Extended version available as Technical Report UCB/ERL M05/32 (pdf, ps).
Type-Based Verification of Assembly Language: Bor-Yuh Evan Chang (2005)
MS Thesis.
Inferring Object Invariants (ps): Bor-Yuh Evan Chang and K. Rustan M. Leino (2005)
First International Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL'05), ENTCS, ©Elsevier.
Type-Based Verification of Assembly Language for Compiler Debugging (ps): Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, and Robert R. Schneck (2005)
Second Workshop on Types in Language Design and Implementation (TLDI'05), ©ACM.
The Open Verifier Framework for Foundational Verifiers (ps): Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, and Robert R. Schneck (2005)
Second Workshop on Types in Language Design and Implementation (TLDI'05), ©ACM.
Abstract Interpretation with Alien Expressions and Heap Structures (ps): Bor-Yuh Evan Chang and K. Rustan M. Leino (2005)
Sixth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'05), LNCS, ©Springer-Verlag.
Extended version available as Technical Report MSR-TR-2004-115.
PML: Toward a High-Level Formal Language for Biological Systems (ps): Bor-Yuh Evan Chang and Manu Sridharan (2003)
Workshop on Concurrent Models in Molecular Biology (BioConcur), ENTCS, ©Elsevier.
Extended version available as Technical Report UCB/CSD-03-1251 (pdf, ps).
A Judgmental Analysis of Linear Logic (ps): Bor-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning (2003)
Technical Report CMU-CS-03-131R, April 2003, December 2003 (revised). Submitted for publication.
Trustless Grid Computing in ConCert (ps): Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, and Frank Pfenning (2002)
The Third International Workshop on Grid Computing (GRID 2002).
Towards a Functional Library for Fault-Tolerant Grid Computing (ps): Bor-Yuh Evan Chang, Margaret DeLap, Jason Liszka, Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning (2002)
Unpublished work-in-progress paper.
Iktara in ConCert: Realizing a Certified Grid Computing Framework from a Programmer's Perspective (ps): Bor-Yuh Evan Chang (2002)
Senior Thesis. Available as Technical Report CMU-CS-02-150.
Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic (ps): Andreas Abel, Bor-Yuh Evan Chang, and Frank Pfenning (2001)
Workshop on Proof Transformations, Proof Presentations, and Complexity of Proofs (PTP-01).