Bor-Yuh Evan Chang

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2008-161

December 15, 2008

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-161.pdf

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 or as broadly applied as they could be because for the most part, they are considered expert tools.

Because of fundamental limitations in what can be computed automatically, all program analyzers must incorporate some amount of domain-specific knowledge. Typically, such domain-specific knowledge is either provided by expert-user specification or built directly into the analyzer. The former approach often expects a high-level of program analysis expertise, while the latter does not allow for any input from the program developer--the person who best understands the code being analyzed. Instead, we advocate a more flexible view where we look to users to cooperate with the analyzer but without expecting them to be program analysis experts. That is, we make progress towards <i>end-user program analysis</i> where non-experts can interact with an analyzer to provide the domain-specific knowledge it needs in order to give users the analysis results they want.

In particular, this dissertation presents a new technique, based on the end-user approach, for precise program analysis in the presence of data structures. Program analyzers that reason precisely about data structures have typically required sophisticated (and thus often burdensome) logical invariant specifications from the user. Instead, 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.

Our technique 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 specifications in order to make them useful for static program analysis.

Advisors: George Necula

---

BibTeX citation:

@phdthesis{Chang:EECS-2008-161,
    Author= {Chang, Bor-Yuh Evan},
    Title= {End-User Program Analysis},
    School= {EECS Department, University of California, Berkeley},
    Year= {2008},
    Month= {Dec},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-161.html},
    Number= {UCB/EECS-2008-161},
    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 or as broadly applied as they could be because for the most part, they are considered expert tools.

Because of fundamental limitations in what can be computed automatically, all program analyzers must incorporate some amount of domain-specific knowledge.  Typically, such domain-specific knowledge is either provided by expert-user specification or built directly into the analyzer.  The former approach often expects a high-level of program analysis expertise, while the latter does not allow for any input from the program developer--the person who best understands the code being analyzed.  Instead, we advocate a more flexible view where we look to users to cooperate with the analyzer but without expecting them to be program analysis experts.  That is, we make progress towards <i>end-user program analysis</i> where non-experts can interact with an analyzer to provide the domain-specific knowledge it needs in order to give users the analysis results they want.

In particular, this dissertation presents a new technique, based on the end-user approach, for precise program analysis in the presence of data structures. Program analyzers that reason precisely about data structures have typically required sophisticated (and thus often burdensome) logical invariant specifications from the user.  Instead, 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.

Our technique 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 specifications in order to make them useful for static program analysis.},
}

EndNote citation:

%0 Thesis
%A Chang, Bor-Yuh Evan 
%T End-User Program Analysis
%I EECS Department, University of California, Berkeley
%D 2008
%8 December 15
%@ UCB/EECS-2008-161
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-161.html
%F Chang:EECS-2008-161