Faculty Candidate: Viktor Kuncak/Electrical Engineering and Computer Science Department MIT Modular Static Analysis with Sets and Relations in ACES 2.302

Contact Name: 
Jenna Whitney
Date: 
Apr 20, 2006 11:00am - 12:00pm


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

s and their sizes and new approaches for extending
the applicability o

f existing reasoning techniques. We successfully
used our system to ver

ify data structure consistency properties
of examples based on computer
games web servers and numerical
simulations. We have verified imple

mentations and
uses of data structures such as linked lists with back po

inters
and iterators trees with parent pointers two-level skip
li

sts array-based data structures as well as combinations
of these data
structures. This talk presents our experience
in developing the syste

m and using the system to build verified software.