Publication detail

Abstract Regular Model Checking

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

Original Title

Abstract Regular Model Checking

Type

journal article in Scopus

Language

English

Original Abstract

We propose abstract regular model checking as a new generic techniquefor verification of parametric and infinite-state systems. Thetechnique combines the two approaches of regular model checking andverification by abstraction. We propose a general framework of themethod as well as several concrete ways of abstracting automata ortransducers, which we use for modelling systems and encoding sets oftheir configurations as usual in regular model checking. Theabstraction is based on collapsing states of automata (or transducers)and its precision is being incrementally adjusted by analysing spuriouscounterexamples. We illustrate the technique on verification of a widerange of systems including a novel application of automata-basedtechniques to an example of systems with dynamic linked data structures.

Keywords

formal verification, infinite-state and parameterized systems, regular model checking, abstraction

Authors

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

RIV year

2004

Released

2. 4. 2004

Publisher

Springer Verlag

Location

Berlin

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Year of study

2004

Number

3114

State

Federal Republic of Germany

Pages from

372

Pages to

386

Pages count

15

URL

http://www.fit.vutbr.cz/~vojnar/Publications/bhv-armc-04.ps.gz

BibTex

@article{BUT45718,
  author="Ahmed {Bouajjani} and Peter {Habermehl} and Tomáš {Vojnar}",
  title="Abstract Regular Model Checking",
  journal="Lecture Notes in Computer Science",
  year="2004",
  volume="2004",
  number="3114",
  pages="372--386",
  doi="10.1007/978-3-540-27813-9\{_}29",
  issn="0302-9743",
  url="http://www.fit.vutbr.cz/~vojnar/Publications/bhv-armc-04.ps.gz"
}