Detail publikačního výsledku

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

Anglický název

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

Druh

Článek recenzovaný mimo WoS a Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

formal verification, program analysis, dynamic linked data structures

Klíčová slova v angličtině

formal verification, program analysis, dynamic linked data structures

Autoři

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

Vydáno

14.01.2006

Kniha

Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS 2005)

ISSN

1571-0661

Periodikum

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

Svazek

2006

Číslo

145

Stát

Spojené státy americké

Strany od

113

Strany do

130

Strany počet

18

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

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"
}