[Pl-seminar] Thesis Defense: Automating Modular Program Verification by Refining Specifications TODAY

Mitchell Wand wand at ccs.neu.edu
Tue Dec 4 09:27:49 EST 2007

..sorry about the short notice.  --Mitch

Thesis Defense: Automating Modular Program Verification by Refining
Speaker: Mana Taghdiri
Speaker Affiliation: Software Design Group   MIT CSAIL
Host: Daniel Jackson
Host Affiliation: MIT CSAIL

Date: 12-4-2007
Time: 2:00 PM - 3:00 PM
Refreshments: 1:45 PM
Location: 32-G449 (Kiva/Patil)

Modular analyses of software systems rely on the specifications of the
modules. In many analysis techniques (e.g. ESC/Java), the specifications
to be provided by users. This puts a considerable burden on users and thus
limits the applicability of such techniques. To avoid this problem, some
analysis techniques automatically extract module summaries that capture
aspects of the modules' behaviors. However, such summaries are only useful
checking a restricted class of properties.

We describe a static modular analysis that automatically extracts procedure
specifications in order to check heap-manipulating programs against rich
structure properties. Extracted specifications are context-dependent; their
precision depends on both the property being checked, and the calling
in which they are used. Starting from a rough over-approximation of the
behavior of each call site, our analysis computes an abstraction of the
procedure being analyzed and checks it against the property. Specifications
further refined, as needed, in response to spurious counterexamples. The
analysis terminates when either the property has been validated (with
to a finite domain), or a non-spurious counterexample has been found.

Furthermore, we describe a lightweight static technique to extract
specifications of heap-manipulating procedures. These specifications neither
context-dependent, nor require any domain finitizations. They summarize the
general behavior of procedures in terms of their effect on program state.
They bound the values of all variables and fields in the post-state of the
procedure by relational expressions in terms of their values in the
The analysis maintains both upper and lower bounds so that in some cases an
exact result can be obtained.

Relevant URL(S):
For more information please contact: Maria Rebelo, 3-5895, mr at csail.mit.edu
-------------- next part --------------
HTML attachment scrubbed and removed

More information about the pl-seminar mailing list