[Pl-seminar] Fwd: TALK:Friday 9-29-06 THESIS DEFENSE: Decision Procedures for Modular Da

[Mitchell Wand]

In case you didn't get this already...  --Mitch

---------- Forwarded message ----------
From: CSAIL Event Calendar <eventcalendar at csail.mit.edu>
Date: Sep 25, 2006 9:18 AM
Subject: TALK:Friday 9-29-06 THESIS DEFENSE: Decision Procedures for Modular
Da
To: seminars at csail.mit.edu


THESIS DEFENSE: Decision Procedures for Modular Data Structure Verification
Speaker: Viktor Kuncak
Speaker Affiliation: CSAIL
Host: Professor Martin Rinard
Host Affiliation: MIT-CSAIL

Date: 9-29-2006
Time: 2:00 PM - 3:00 PM
Refreshments: 1:45 PM
Location: 32-G449 Patil/Kiva Conference Room

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.

Relevant URL(S):
For more information please contact: Mary McDavitt, 617-253-9620,
mmcdavit at csail.mit.edu

_______________________________________________
Seminars mailing list
Seminars at lists.csail.mit.edu
https://lists.csail.mit.edu/mailman/listinfo/seminars
-------------- next part --------------
HTML attachment scrubbed and removed