[Pl-seminar] Interesting talk THIS MORNING

[Mitchell Wand]

Thesis Defense: Verification of Full Functional Correctness for Imperative
Linked Data Structures
Speaker: Karen Zee
Speaker Affiliation: Ph.D. Candidate, CSAIL
Host: Martin Rinard
Host Affiliation: MIT-CSAIL

Date: 12-16-2009
Time: 11:00 AM - 12:00 PM
Refreshments: 10:45 AM
Location: 32-G449 - Patil/Kiva Conference Room

We present the verification of full functional correctness for a collection
of
imperative linked data structure implementations. Data structures are good
candidates for full functional verification because of their prevalence in
modern software systems and because their interfaces are generally
well-understood. At the same time, imperative linked data structures present
special challenges. Due to the phenomena of aliasing and indirection, many
of
the desired correctness properties involve logical constructs that are known
to be intractable for automated reasoning systems. In the past, researchers
have either focused on partial correctness properties or embraced the
necessary developer effort through the use of interactive theorem
proving tools.

We adopt a hybrid approach that takes advantage of automated reasoning
techniques but also enables developers to direct the efforts of the
automated
reasoning systems where necessary to resolve difficult proof tasks. Jahob is
a
program verification system that uses the standard specification and
verification paradigm, but is unique in its use of an integrated reasoning
approach and proof language. Instead of using a single monolithic prover,
Jahob includes interfaces to a diverse collection of automated reasoning
systems---automated theorem provers, decision procedures, and program
analyses---that work together to prove the verification conditions that the
system automatically generates. Jahob also incorporates a declarative proof
language that enables the developer to direct the efforts of the automated
reasoning systems to successfully verify properties that the system is
unable
to verify without guidance.

We have used Jahob to verify the full functional correctness of a collection
of imperative linked data structures implemented in Java. Our specifications
characterize the behavior of the data structures in terms of their abstract
state, resulting in verified interfaces that can be used to reason about the
behavior of the data structures without revealing the underlying
representation. The results demonstrate the effectiveness of our hybrid
approach and provide valuable insight into the specification and
verification
of imperative linked data structures.

Relevant URL(S):
For more information please contact: Mary McDavitt, 617-253-9620,
mmcdavit at csail.mit.edu
-------------- next part --------------
HTML attachment scrubbed and removed