Computer Science Colloquium

Modular Static Analysis with Sets and Relations

Victor Kuncak
MIT

May 1, 2006 11:45 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185

Directions: http://cs.nyu.edu/csweb/Location/directions.html
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html

Hosts:

Clark Barrettbarrett@cs.nyu.edu, (212) 998-3105

Abstract

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.

Bio

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.


top | contact webmaster@cs.nyu.edu