THESIS DEFENSE: Decision Procedures for Modular Data Structure Verification
Speaker: Viktor Kuncak , CSAIL
Date: September 29 2006
Time: 2:00PM to 3:00PM
Location: 32-G449 Patil/Kiva Conference Room
Host: Professor Martin Rinard, MIT-CSAIL
Contact: Mary McDavitt, 617-253-9620, mmcdavit@csail.mit.edu
ABSTRACT:
I describe the foundations and the design of the Jahob
verificaton system. Jahob can verify properties of Java
programs with dynamically allocated data structures such as
trees, lists, and hash tables. Jahob verifies that data
structure operations correctly implement their
specifications (for example, an insertion or removal on a
data structure instance correctly change the (key,value) map
specifying the content of the instance and preserve the
content of all other instances); that operations preserve
data structure representation invariants (for example, hash
table elements are stored in appropriate buckets, a binary
tree is sorted and does not have cycles); that data
structure clients correctly use the data structures (for
example, the client does not call remove operation on an
empty data structure); and that there are no run-time errors
such as null dereference, type cast, or array out of bounds
errors.
Developers write Jahob specifications in a variant of
classical higher-order logic (HOL). Jahob uses these
specifications for modular verification. Jahob reduces the
verification problem to validity of HOL formulas. As the
main contribution, I show how to prove interesting
subclasses of formulas in this logic by approximating them
with formulas in more tractable fragments and combining
different approximations in a synergistic way. I describe a
technique based on a translation to first-order logic, a
technique that extends the range of applicability of
existing logics, and a new implementation and complexity
analysis of a logic that combines Boolean Algebra with
Presburger Arithmetic.
See other events that are part of
See other events happening in September 2006
