Publication Details

Abstract Regular Model Checking

BOUAJJANI Ahmed, HABERMEHL Peter and VOJNAR Tomáš. Abstract Regular Model Checking. Lecture Notes in Computer Science, vol. 2004, no. 3114, pp. 372-386. ISSN 0302-9743.
Czech title
Abstraktní regulární model checking
Type
journal article
Language
english
Authors
Bouajjani Ahmed (UPAR7)
Habermehl Peter (UPAR7)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

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

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.

Published
2004
Pages
372-386
Journal
Lecture Notes in Computer Science, vol. 2004, no. 3114, ISSN 0302-9743
Book
Computer Aided Verification
Publisher
Springer Verlag
Place
Berlin, DE
DOI
EID Scopus
BibTeX
@ARTICLE{FITPUB7410,
   author = "Ahmed Bouajjani and Peter Habermehl and Tom\'{a}\v{s} Vojnar",
   title = "Abstract Regular Model Checking",
   pages = "372--386",
   booktitle = "Computer Aided Verification",
   journal = "Lecture Notes in Computer Science",
   volume = 2004,
   number = 3114,
   year = 2004,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-540-27813-9\_29",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7410"
}
Back to top