Colloquium: Viktor Kuncak MIT & EPFL Automated Reasoning for Data Structure Verification in ACES 2.402

Contact Name: 
Jenna Whitney
Jan 23, 2007 2:00pm - 3:00pm

Sign up schedule:


br>Speaker Name/Affiliation: Viktor Kuncak MIT and EPFL


January 23 2007 2:00p.m.-3:00p.m.

Coffee & Refreshments: 1:45pm

ACES 2.402

Host: Jayadev Misra

Title: Automated Reasonin

g for Data Structure Verification

I describe our ongoing effort to b

uild Jahob an automated
verification system for Java programs. We hav

e used Jahob
to successfully verify that dynamically allocated data str

such as trees lists and hash tables conform to their specific

(given in terms of method contracts and invariants). Developers

write Jahob specifications in classical higher-order logic
Jahob uses these specifications for modular verification.
Jahob reduce

s the verification of each Java method to the
problem of proving the va

lidity of an HOL formula.

Jahob proves the validity of HOL formulas

by combining a
number of decision procedures and theorem provers. I de

Jahob''s approach for combining different reasoning techniques.

I then describe a new decision procedure for quantifier-free

n Algebra with Presburger Arithmetic which enables
reasoning about the
sizes of data structures. The complexity
of this decision procedure i

s optimal and is an exponential
improvement over previous approaches.