Automata-Based Techniques for the Verification of Programs with Linked Data Structures

We propose an approach for the automatic analysis of programs with dynamic linked structures using finite-state word/tree automata as representations for (potentially infinite) sets of heap structures. A heap of a given program is encoded as a word or a tree over an appropriate alphabet, and each statement in the program is translated into a transducer defining a transformation on the heap encodings.

Then, iterative reachability analysis is performed using automata techniques in order to compute an upper-approximation of the set of all reachable heap configurations. The reachability analysis uses abstractions on automata representations (corresponding to finite index equivalence relations on their state space) allowing to speed up the fixpoint computation and to force termination. Automatic abstraction refinement is applied by need based on conterexample analysis. The proposed approach has been implemented and applied to several non trivial examples of programs.

This is a joint work with Peter Habermehl, Pierre Moro, Adam Rogalewicz, and Tomas Vojnar.