Detail publikačního výsledku

Abstract Regular Model Checking

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

Originální název

Abstract Regular Model Checking

Anglický název

Abstract Regular Model Checking

Druh

Článek Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

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

Klíčová slova v angličtině

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

Autoři

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

Rok RIV

2011

Vydáno

02.04.2004

Nakladatel

Springer Verlag

Místo

Berlin

Kniha

Computer Aided Verification

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Svazek

2004

Číslo

3114

Stát

Spolková republika Německo

Strany od

372

Strany do

386

Strany počet

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