Sign up schedule:
http://www.cs.utexas.edu/dep

artment/webevent/utcs/events/cgi/show_schedule.cgi?person=ViktorKuncak
<

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

Date/Time:

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

uctures
such as trees lists and hash tables conform to their specific

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

write Jahob specifications in classical higher-order logic
(HOL).
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

scribe
Jahob''s approach for combining different reasoning techniques.

I then describe a new decision procedure for quantifier-free
Boolea

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.