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. © Springer-Verlag Berlin Heidelberg 2004.
CITATION STYLE
Bouajjani, A., Habermehl, P., & Vojnar, T. (2004). Abstract regular model checking. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3114, 372–386. https://doi.org/10.1007/978-3-540-27813-9_29
Mendeley helps you to discover research relevant for your work.