» Home › Papers › Talks
Department of Computer Science
College of Engineering and Applied Science
University of Colorado at Boulder

office ECOT 621
mail   430 UCB, Boulder, CO 80309-0430 USA
phone +1 (303) 492-8894
fax +1 (303) 492-2844

About Me

I work 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.

I recently completed my Ph.D. with George Necula in the EECS department at the University of California, Berkeley. I also spent the fall of 2008 as a post-doc with Jeff Foster in the PLUM group at the University of Maryland, College Park.

I am looking for enthusiastic students interested in working with me on research projects in programming languages and software systems. If you are interested in finding out more, please contact me.

[curriculum vitae]

top

Teaching

Principles of Programming Languages (CSCI 3155)
Fall 2009
Fundamentals of Programming Languages (CSCI 5535)
Spring 2009
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

Gradual Programming: Bridging the Semantic Gap (Position Paper)
Bor-Yuh Evan Chang, Amer Diwan, and Jeremy G. Siek (2009)
Fun Ideas and Thoughts Session (FIT) at the 2009 Conference on Programming Language Design and Implementation (PLDI'09)
End-User Program Analysis (ps)
Bor-Yuh Evan Chang (2008)
Ph.D. Dissertation. Also available as Technical Report UCB/EECS-2008-161.
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)
M.S. 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

End-User Shape Analysis (ppt, flash)
August 11, 2009
National Taiwan University
Using Checkers for End-User Shape Analysis (ppt, flash)
August 11, 2009
National Taiwan University
Reduction in End-User Shape Analysis (ppt, flash)
July 24, 2009
Dagstuhl Seminar 09301: Typing, Analysis, and Verification of Heap-Manipulating Programs
Gradual Programming: Bridging the Semantic Gap (ppt, pdf, flash)
June 16, 2009
Fun Ideas and Thoughts Session (FIT) at the 2009 Conference on Programming Language Design and Implementation (PLDI'09)
Dublin, Ireland
End-User Program Analysis for Data Structures (ppt)
November 24, 2008
University of Virginia
End-User Program Analysis (ppt)
August 28, 2008
Dissertation Talk
University of California, Berkeley
Extensible Shape Analysis by Designing with the User in Mind (ppt)
May 16, 2008
Open Source Quality Project Retreat
Santa Cruz, California, USA
Precise Program Analysis with Data Structures (ppt)
February-April 2008
Job Talk
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    ph.d. advisor (August 2002 - August 2008)
K. Rustan M. Leino    internship mentor (May 2004 - August 2005)
Bob Harper    undergraduate advisor (August 2001 - June 2002)
Frank Pfenning    undergraduate advisor (January 2001 - June 2002)