Towards a Systematic Framework for Automatic Pattern-Based Verification of Dynamic Data Structures

pattern-based verification, infinite state space, abstraction

This paper aims at automatic verification of programs working with possibly unbounded dynamic data structures. Namely, it concentrates on pattern-based verification, which is an automatic verification technique usable in this area. Its abstraction consists in clustering isomorphic subgraphs of the structure into so-called summary nodes. The behaviour of the program is then simulated on created summarized shape graphs, which allows to work with unbounded structures. The technique detects errors like dereference over NULL, memory  leakage etc.

This paper gives a theoretical support to pattern-based verification, i.e. the basic notions and their properties are formalized, their practical value is shown, the class of structures, which pattern-based verification can handle, is specified and at the end of the paper some proofs are shown, which demonstrates usability of this technique.