[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, 5/17/06
11:45-1:30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Modular Static Analysis with Sets and Relations

Viktor Kuncak
MIT CSAIL


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.

ABOUT THE SPEAKER: Viktor Kuncak is a Ph.D. candidate in the MIT
Computer Science and Artificial Intelligence Lab.  His interests
include program analysis and verification, formal methods, programming
languages, and software engineering.
				   

Upcoming Events:

stay tuned...

--Mitch