Precise and Fully-Automatic Verification of Container-Manipulating Programs

One of the key challenges in automated software verification is obtaining a conservative yet sufficiently precise understanding of the contents of data structures in the heap. A particularly important and widely-used class of heap data structures is containers, which support operations such as inserting, retrieving, removing, and iterating over elements. Examples of containers include arrays, lists, vectors, sets, maps, stacks, queues, etc.

In this talk, I will describe a sound, precise, scalable, and fully-automatic static analysis technique for reasoning about the contents of container data structures. This technique is capable of tracking position-value and key-value correlations, supports reasoning about arbitrary nestings of these data structures, and integrates container reasoning directly into a heap analysis, allowing, for the first time, the verification of complex programs that manipulate heap objects through container data structures. More specifically, I will describe a symbolic heap abstraction that augments a graph representation of the heap with logical formulas and that reduces some of the difficulty of heap reasoning to standard logic operations, such as existential quantifier elimination and satisfiability. I will present experimental results demonstrating that our technique is very useful for verifying memory safety in complex heap- and container-manipulating C and C++ programs that use arrays and other container data structures from the STL and QT libraries.
Thomas Dillig is an assistant professor at the College of William & Mary. He obtained a PhD in computer science from Stanford University in 2012. The goal of Tom's research is to make programs more reliable through static reasoning. Specifically, Tom is interested in developing precise static analysis techniques that work on real programs. Tom is also interested in constraint solving and simplification techniques and applying them to program analysis problems.