Bor-Yuh Evan Chang

Department of Electrical Engineering and Computer Science

Berkeley, CA U.S.A.

School [map]	Home [map]
447 Soda Hall	1771 Highland Pl., Apt. 5
Berkeley, CA 94720-1776	Berkeley, CA 94709-1064
+1 (510) 642-3979	+1 (510) 841-0807

About Me

I am completing my Ph.D. with George Necula in the EECS department at the University of California, Berkeley working primarily in the areas of programming languages and program analysis. My research interests center on tools and techniques for building, understanding, and ensuring reliable computational systems. Currently, my focus is on using novel ways of interacting with the programmer to design more precise and practical program analyses. The Xisa project is an instance of this approach that infers precise properties of complex data structure manipulations. The novelty of Xisa is that it extracts both the necessary invariants and reasoning rules from executable assertions (analogous to data structure validation code often written for testing). This approach allows the developer to focus the analysis to the properties of interest and without using a separate formalism for testing and static analysis.

During the fall of 2008, I am visiting Jeff Foster and the PLUM group at the University of Maryland, College Park. In January 2009, I will be an assistant professor of Computer Science at the University of Colorado, Boulder.

[curriculum vitae]

top

Selected Projects

Xisa: Extensible Inductive Shape Analysis
Efficient algorithms and automatic tools for reasoning about heap-manipulating programs, such as those that use recursive data structures like pointer-based lists and trees.
Papers: POPL'08, SAS'07.

top

Recent 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).
[more]

top

Recent Talks

Relational Inductive Shape Analysis (ppt): January 11, 2008
Thirty-Fifth Symposium on Principles of Programming Languages (POPL'08)
San Francisco, California, USA
Materialization in Shape Analysis with Structural Invariant Checkers (pdf): August 27, 2007
IT University of Copenhagen
Shape Analysis with Structural Invariant Checkers (pdf): August 24, 2007
Fourteenth International Static Analysis Symposium (SAS'07)
Kongens Lyngby, Denmark
Analysis of Low-Level Code Using Cooperating Decompilers (pdf): August 31, 2006
Thirteenth International Static Analysis Symposium (SAS'06)
Seoul, Korea
Inferring Object Invariants (html-ie, pdf, ps): January 21, 2005
First International Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL'05)
Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05)
Paris, France
Abstract Interpretation with Alien Expressions and Heap Structures (html-ie, pdf, ps): January 18, 2005
Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05)
Paris, France
Type-Based Verification of Assembly Language for Compiler Debugging (html-ie, pdf, ps): January 10, 2005
Second Workshop on Types in Language Design and Implementation (TLDI'05)
Thirty-Second Symposium on Principles of Programming Languages (POPL'05)
Long Beach, California, USA
PML: Toward a High-Level Formal Language for Biological Systems: September 6, 2003
Workshop on Concurrent Models in Molecular Biology (BioConcur)
International Conference on Concurrency Theory (CONCUR '03)
Marseille, France
[more]

top

Conferences

PLDI'09 June 15-20, 2009 Dublin, Ireland External Review Committee Member: ACM SIGPLAN 2009 Conference on Programming Language Design and Implementation
AIOOL'05 January 21, 2005 Paris, France PC Member: 1st International Workshop on Abstract Interpretation of Object-Oriented Languages

top

Advisors

George Necula    advisor (August 2002 - present)

K. Rustan M. Leino    mentor (May 2004 - August 2004)

Bob Harper    advisor (August 2001 - June 2002)

Frank Pfenning    advisor (January 2001 - June 2002)

Andreas Abel    mentor (January 2001 - June 2001)

top

Teaching

Programming Languages and Compilers (CS164): Spring 2004, assisting George Necula.
Principles of Programming (15-212): Fall 2000, assisting Karl Crary and John Lafferty.
Fundamental Structures of Computer Science I (15-211): Spring 2000, assisting Klaus Sutner.
Mathematical Foundations of Computer Science (15-151): Fall 1999, assisting Edmund Clarke and Klaus Sutner.

George Necula		advisor (August 2002 - present)
K. Rustan M. Leino		mentor (May 2004 - August 2004)
Bob Harper		advisor (August 2001 - June 2002)
Frank Pfenning		advisor (January 2001 - June 2002)
Andreas Abel		mentor (January 2001 - June 2001)