Abstract Regular Model Checking

13 years 11 months ago
Abstract Regular Model Checking
Regular Tree Model Checking Ahmed Bouajjani, Peter Habermehl 1 LIAFA, University Paris 7, Case 7014, 2, place Jussieu, F-75251 Paris Cedex 05, France Adam Rogalewicz, Tom´aˇs Vojnar 2 FIT, Brno University of Technology, Boˇzetˇechova 2, CZ-61266, Brno, Czech Republic Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the sobstract regular m...
Ahmed Bouajjani, Peter Habermehl, Tomás Voj
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CAV
Authors Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar
Comments (0)