Colloquium
Bor-Yuh "Evan" Chang
EECS Department
UC Berkeley
Wednesday, April 2, 2008
3147 MEB
Refreshments 3:20 p.m.
Lecture 3:40 p.m.
Host: John Regehr
Evan's schedule
Title: Precise Program Analysis with Data Structures
Abstract
Program analysis tools are being adopted by industry to improve the reliability and overall quality of software like never before because they can rule out entire classes of errors. Yet, today's tools are far from being as effective as they could be, for almost all program analyses have difficulty when objects of interest are put into data structures. Program analyses that reason precisely about data structures typically require sophisticated (and thus often burdensome) logical invariant specifications from the user. We propose a novel way to involve the user in guiding the analysis by extracting both the necessary invariants and reasoning rules from executable assertions in the code.
In this talk, I describe a new technique for precise program analysis in the presence of data structures. It is based on data structure validation code that is often written anyway for testing purposes. From the developer's perspective, such validation code provides guidance to the analysis in a familiar style, and we show how our analysis results can be rendered graphically in a form that is comparable to what might be drawn on a whiteboard or printed in a textbook. From the analysis tool's perspective, data structure validation code provides the essential ingredients for a good abstraction that precisely represents the important facts while ignoring irrelevant details. The crucial innovations in our system are automatic methods for understanding and generalizing the developer-provided data structure validation code to make them useful for static program analysis. Example results produced by our analysis tool, Xisa, are available at http://xisa.cs.berkeley.edu/.
Bio
Bor-Yuh Evan Chang is completing his Ph.D. with George Necula at the University of California, Berkeley working in the areas of programming languages and program analysis. He is interested in tools and techniques for building, understanding, and ensuring reliable computational systems. His current focus is on using novel ways of interacting with the programmer to design more precise and practical program analyses.
Return to 2008 Events Calendar
Program analysis tools are being adopted by industry to improve the reliability and overall quality of software like never before because they can rule out entire classes of errors. Yet, today's tools are far from being as effective as they could be, for almost all program analyses have difficulty when objects of interest are put into data structures. Program analyses that reason precisely about data structures typically require sophisticated (and thus often burdensome) logical invariant specifications from the user. We propose a novel way to involve the user in guiding the analysis by extracting both the necessary invariants and reasoning rules from executable assertions in the code.
In this talk, I describe a new technique for precise program analysis in the presence of data structures. It is based on data structure validation code that is often written anyway for testing purposes. From the developer's perspective, such validation code provides guidance to the analysis in a familiar style, and we show how our analysis results can be rendered graphically in a form that is comparable to what might be drawn on a whiteboard or printed in a textbook. From the analysis tool's perspective, data structure validation code provides the essential ingredients for a good abstraction that precisely represents the important facts while ignoring irrelevant details. The crucial innovations in our system are automatic methods for understanding and generalizing the developer-provided data structure validation code to make them useful for static program analysis. Example results produced by our analysis tool, Xisa, are available at http://xisa.cs.berkeley.edu/.
Bio
Bor-Yuh Evan Chang is completing his Ph.D. with George Necula at the University of California, Berkeley working in the areas of programming languages and program analysis. He is interested in tools and techniques for building, understanding, and ensuring reliable computational systems. His current focus is on using novel ways of interacting with the programmer to design more precise and practical program analyses.
Return to 2008 Events Calendar