There is a signup schedule for this e

vent.

Speaker Name/Affiliation: Viktor Kuncak/Electrical Engineerin

g and Computer Science Department MIT

Talk Title: Modular Static A

nalysis with Sets and Relations

Date/Time: April 20 2006 at 11:00

a.m.

Coffee: 10:45 a.m.

Location: ACES 2.302

Host: K

athryn McKinley

Talk Abstract:
We present a new approach for stat

ically analyzing data structure
consistency properties. Our approach i

s based on specifying
interfaces of data structures using abstract sets
and relations.
This enables our system to independently verify that

1) each data structure satisfies internal consistency properties
a

nd each data structure
operation conforms to its interface;

2) t

he application uses each data structure interface correctly
and mainta

ins the desired
global consistency properties that cut across multiple d

ata
structures.

Our system verifies these properties by combinin

g static
analyses constraint solving algorithms and theorem provers

promising an unprecedented combination of precision and
scalability

. The combination of different techniques is
possible because all syst

em components use a common specification
language based on sets and rel

ations.

In the context of our system we developed new algorithms for computing loop invariants new techniques for reasoning
about set

m and using the system to build verified software.