Campus Event Calendar

Event Entry

New for: D1, D2, D3, D4, D5

What and Who

Modular Static Analysis with Sets and Relations

Viktor Kuncak
SWS Colloquium
Viktor Kuncak is a Ph.D. candidate in the MIT Computer Science and Artificial Intelligence Lab. His interests include program analysis and verification, software engineering, programming languages and compilers, and formal methods.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS  
Expert Audience

Date, Time and Location

Thursday, 6 April 2006
-- Not specified --
E1 4


We present a new approach for statically analyzing data structure consistency properties.  Our approach is 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 and each data structure operation conforms to its interface;

2) the application uses each data structure interface correctly, and maintains the desired global consistency properties that cut across multiple data structures.

Our system verifies these properties by combining 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 system components use a common specification language based on sets and relations.

In the context of our system, we developed new algorithms for computing loop invariants, new techniques for reasoning about sets and their sizes, and new approaches for extending the applicability of existing reasoning techniques. We successfully used our system to verify data structure consistency properties of examples based on computer games, web servers, and numerical simulations.  We have verified implementations and uses of data structures such as linked lists with back pointers and iterators, trees with parent pointers, two-level skip lists, array-based data structures, as well as combinations of these data structures. This talk presents our experience in developing the system and using the system to build verified software.


--email hidden
passcode not visible
logged in users only

Carina Schmitt, 05/10/2006 11:21
Brigitta Hansen, 04/03/2006 16:57 -- Created document.