Publication detail

Abstract Regular Model Checking

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

Original Title

Abstract Regular Model Checking

English Title

Abstract Regular Model Checking

Type

journal article - other

Language

en

Original Abstract

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

English abstract

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

Keywords

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

RIV year

2004

Released

02.04.2004

Publisher

Springer Verlag

Location

Berlin

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Year of study

2004

Number

3114

State

DE

Pages from

372

Pages to

386

Pages count

15

URL

Documents

BibTex


@article{BUT45718,
  author="Ahmed {Bouajjani} and Peter {Habermehl} and Tomáš {Vojnar}",
  title="Abstract Regular Model Checking",
  annote="We propose abstract regular model checking as a new generic technique
for verification of parametric and infinite-state systems. The
technique combines the two approaches of regular model checking and
verification by abstraction. We propose a general framework of the
method as well as several concrete ways of abstracting automata or
transducers, which we use for modelling systems and encoding sets of
their configurations as usual in regular model checking. The
abstraction is based on collapsing states of automata (or transducers)
and its precision is being incrementally adjusted by analysing spurious
counterexamples. We illustrate the technique on verification of a wide
range of systems including a novel application of automata-based
techniques to an example of systems with dynamic linked data structures.",
  address="Springer Verlag",
  booktitle="Computer Aided Verification",
  chapter="45718",
  institution="Springer Verlag",
  journal="Lecture Notes in Computer Science",
  number="3114",
  volume="2004",
  year="2004",
  month="april",
  pages="372--386",
  publisher="Springer Verlag",
  type="journal article - other"
}