Detail publikace

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

VOJNAR, T. ČEŠKA, M. ERLEBACH, P.

Originální název

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

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

formal verification, program analysis, dynamic linked data structures

Autoři

VOJNAR, T.; ČEŠKA, M.; ERLEBACH, P.

Rok RIV

2005

Vydáno

12. 9. 2005

Místo

Warwick

Strany od

101

Strany do

117

Strany počet

17

BibTex

@inproceedings{BUT18064,
  author="Tomáš {Vojnar} and Milan {Češka} and Pavel {Erlebach}",
  title="Pattern-Based Verification of Programs with Extended Linear Linked Data Structures",
  booktitle="Proceedings of Fifth International Workshop on Automated Verification of Critical Systems",
  year="2005",
  pages="101--117",
  address="Warwick"
}