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, software engineering, programming
languages and compilers, and formal methods.