Detail publikace

Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking

VOJNAR, T. BOUAJJANI, A. HABERMEHL, P. MORO, P.

Originální název

Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking

Typ

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

Jazyk

angličtina

Originální abstrakt

We address the problem of automatic verification of programs withdynamic data structures. We consider the case of sequential,non-recursive programs manipulating 1-selector-linked structures suchas traditional linked lists (possibly sharing their tails) and circularlists. We propose an automata-based approach for a symbolicverification of such programs using the regular model checkingframework. Given a program, the configurations of the memory aresystematically encoded as words over a suitable finite alphabet,potentially infinite sets of configurations are represented byfinite-state automata, and statements of the program are automaticallytranslated into finite-state transducers defining regular relationsbetween configurations. Then, abstract regular model checkingtechniques are applied in order to automatically check safetyproperties concerning the shape of the computed configurations orrelating the input and output configurations. For this particularpurpose, we introduce new techniques for the computation ofabstractions of the set of reachable configurations and to refine theseabstractions if spurious counterexamples are detected.  Finally,we present experimental results showing the applicability of theapproach and its efficiency.

Klíčová slova

formal verification, model checking, infinite-state systems, software verification, dynamic data structures

Autoři

VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; MORO, P.

Rok RIV

2005

Vydáno

4. 4. 2005

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-540-25333-4

Kniha

Tools and Algorithms for the Construction and Analysis of Systems

Edice

Lecture Notes in Computer Science

Strany od

13

Strany do

29

Strany počet

17

URL

http://www.fit.vutbr.cz/~vojnar/Publications/bhmv-lists-05.ps.gz

BibTex

@inproceedings{BUT32780,
  author="Tomáš {Vojnar} and Ahmed {Bouajjani} and Peter {Habermehl} and Pierre {Moro}",
  title="Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2005",
  series="Lecture Notes in Computer Science",
  volume="3440",
  pages="13--29",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-25333-4",
  url="http://www.fit.vutbr.cz/~vojnar/Publications/bhmv-lists-05.ps.gz"
}