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

formal verification, program analysis, dynamic 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.