Pattern-Based Verification of Programs with Extended Linear Linked Data Structures

The paper deals with the problem of automatic verification of programswith dynamic linked data structures. In particular, the use ofpattern-based abstraction of memory configurations is considered. Inthis approach, one can abstract memory configurations by abstractingaway the exact number of adjacent occurrences of certain memorypatterns. The paper extends the state-of-the-art in this area byproposing a fully automatic and efficient way of  detecting thememory patterns to be used from the memory  configurations thatthe program at hand is generating. The method targets programsmanipulating a broad class of extended linear linked data structureshaving a linear skeleton (possibly bidirectionally-linked or cyclic)with certain additional pointers defined on top of it, which coversmany practical dynamic data structures (such as lists, doubly-linkedlists, cyclic lists, lists with tail/head pointers, etc.). Theexperimental results obtained from a prototype implementation of themethod show that the method is very competitive and offers a bigpotential for future extensions.