Modular Static Analysis with Sets and Relations

Dr. Kuncak is from MIT
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.