Publication detail

Abstract Regular (Tree) Model Checking

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

Original Title

Abstract Regular (Tree) Model Checking

English Title

Abstract Regular (Tree) Model Checking

Type

journal article - other

Language

en

Original Abstract

Regular model checking is a generic technique for verification of infinite-state and/or parametrised systems which uses finite word automata or finite tree automata to finitely represent potentially infinite sets of reachable configurations of the systems being verified. The problems addressed by regular model checking are typically undecidable. In order to facilitate termination in as many cases as possible, acceleration is needed in the incremental computation of the set of reachable configurations in regular model checking. In this work, we describe how various incrementally refinable abstractions on finite (word and tree) automata can be used for this purpose. Moreover, the use of abstraction does not only increase chances of the technique to terminate, but it also significantly reduces the problem of an explosion in the number of states of the automata that are generated by regular model checking. We illustrate the efficiency of abstract regular (tree) model checking in verification of simple systems with various sources of infinity such as unbounded counters, queues, stacks, and parameters. We then show how abstract regular tree model checking can be used for verification of programs manipulating tree-like dynamic data structures. Even more complex data structures can be handled using a suitable tree-like encoding.

English abstract

Regular model checking is a generic technique for verification of infinite-state and/or parametrised systems which uses finite word automata or finite tree automata to finitely represent potentially infinite sets of reachable configurations of the systems being verified. The problems addressed by regular model checking are typically undecidable. In order to facilitate termination in as many cases as possible, acceleration is needed in the incremental computation of the set of reachable configurations in regular model checking. In this work, we describe how various incrementally refinable abstractions on finite (word and tree) automata can be used for this purpose. Moreover, the use of abstraction does not only increase chances of the technique to terminate, but it also significantly reduces the problem of an explosion in the number of states of the automata that are generated by regular model checking. We illustrate the efficiency of abstract regular (tree) model checking in verification of simple systems with various sources of infinity such as unbounded counters, queues, stacks, and parameters. We then show how abstract regular tree model checking can be used for verification of programs manipulating tree-like dynamic data structures. Even more complex data structures can be handled using a suitable tree-like encoding.

Keywords

Formal verification, Infinite-state and parameterised systems, Programs with dynamic linked data structures, Regular model checking, Abstraction, Finite word and tree automata

RIV year

2012

Released

01.03.2012

Publisher

NEUVEDEN

Location

NEUVEDEN

Pages from

167

Pages to

191

Pages count

25

URL

BibTex


@article{BUT91492,
  author="Adam {Rogalewicz} and Tomáš {Vojnar} and Peter {Habermehl} and Ahmed {Bouajjani}",
  title="Abstract Regular (Tree) Model Checking",
  annote="Regular model checking is a generic technique for verification of infinite-state
and/or parametrised systems which uses finite word automata or finite tree
automata to finitely represent potentially infinite sets of reachable
configurations of the systems being verified. The problems addressed by regular
model checking are typically undecidable. In order to facilitate termination in
as many cases as possible, acceleration is needed in the incremental computation
of the set of reachable configurations in regular model checking. In this work,
we describe how various incrementally refinable abstractions on finite (word and
tree) automata can be used for this purpose. Moreover, the use of abstraction
does not only increase chances of the technique to terminate, but it also
significantly reduces the problem of an explosion in the number of states of the
automata that are generated by regular model checking. We illustrate the
efficiency of abstract regular (tree) model checking in verification of simple
systems with various sources of infinity such as unbounded counters, queues,
stacks, and parameters. We then show how abstract regular tree model checking can
be used for verification of programs manipulating tree-like dynamic data
structures. Even more complex data structures can be handled using a suitable
tree-like encoding.",
  address="NEUVEDEN",
  chapter="91492",
  doi="10.1007/s10009-011-0205-y",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="2",
  volume="14",
  year="2012",
  month="march",
  pages="167--191",
  publisher="NEUVEDEN",
  type="journal article - other"
}