Verifying Programs with Dynamic 1Selector-Linked Structures in Regular Model Checking

Abstract. We address the problem of automatic verification of programs with dynamic data structures. We consider the case of sequential, non-recursive pro-grams manipulating 1-selector-linked structures such as traditional linked lists (possibly sharing their tails) and circular lists. We propose an automata-based approach for a symbolic verification of such programs using the regular model checking framework. Given a program, the configurations of the memory are systematically encoded as words over a suitable finite alphabet, potentially infi-nite sets of configurations are represented by finite-state automata, and statements of the program are automatically translated into finite-state transducers defining regular relations between configurations. Then, abstract regular model checking techniques are applied in order to automatically check safety properties concern-ing the shape of the computed configurations or relating the input and output configurations. For that, we introduce new techniques for the computation of ab-stractions of the set of reachable configurations, and to refine these abstractions if spurious counterexamples are detected. Finally, we present experimental results showing the applicability of the approach and its efficiency.