Publication Details

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

VOJNAR, T.; ČEŠKA, M.; ERLEBACH, P. Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, vol. 2006, no. 145, p. 113-130. ISSN: 1571-0661.
Czech title
Pattern-Based Verification of Programs with Extended Linear Linked Data Structures
Type
journal article
Language
English
Authors
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Češka Milan, prof. RNDr., CSc.
Erlebach Pavel, Ing., Ph.D.
URL
Keywords

formal verification, program analysis, dynamic linked data structures

Abstract

The paper deals with the problem of automatic verification of programs with
dynamic linked data structures. In particular, the use of pattern-based
abstraction of memory configurations is considered. In this approach, one can
abstract memory configurations by abstracting away the exact number of adjacent
occurrences of certain memory patterns. The paper extends the state-of-the-art in
this area by proposing a fully automatic and efficient way of  detecting the
memory patterns to be used from the memory  configurations that the program at
hand is generating. The method targets programs manipulating a broad class of
extended linear linked data structures having a linear skeleton (possibly
bidirectionally-linked or cyclic) with certain additional pointers defined on top
of it, which covers many practical dynamic data structures (such as lists,
doubly-linked lists, cyclic lists, lists with tail/head pointers, etc.). The
experimental results obtained from a prototype implementation of the method show
that the method is very competitive and offers a big potential for future
extensions.

Published
2006
Pages
113–130
Journal
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. 2006, no. 145, ISSN 1571-0661
Book
Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS 2005)
BibTeX 
@article{BUT45072,
  author="Tomáš {Vojnar} and Milan {Češka} and Pavel {Erlebach}",
  title="Pattern-Based Verification of Programs with Extended Linear Linked Data Structures",
  journal="ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE",
  year="2006",
  volume="2006",
  number="145",
  pages="113--130",
  issn="1571-0661",
  url="http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B75H1-4J05Y67-8-1&_cdi=13109&_user=640830&_orig=browse&_coverDate=01%2F14%2F2006&_sk=998549999&view=c&wchp=dGLzVlz-zSkzk&md5=ee9d2a952a112f8b99ffd4cff37e35cd&ie=/sdarticle.pdf"
}
Back to top