. . "25"^^ . "International Journal on Software Tools for Technology Transfer" . "Abstract Regular (Tree) Model Checking"@en . . . "Abstract Regular (Tree) Model Checking" . . "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 o" . . "DE - Spolkov\u00E1 republika N\u011Bmecko" . . . . "120805" . "RIV/00216305:26230/12:PU98200" . . "RIV/00216305:26230/12:PU98200!RIV13-GA0-26230___" . . . . "P(GAP103/10/0306), P(GP201/09/P531), P(MEB021023), P(OC10009), S, Z(MSM0021630528)" . "14" . "http://www.springerlink.com/content/137uu7118p2054j2/" . . "Habermehl, Peter" . . "10.1007/s10009-011-0205-y" . . . "Vojnar, Tom\u00E1\u0161" . "Formal verification, Infinite-state and parameterised systems, Programs with dynamic linked data structures, Regular model checking, Abstraction, Finite word and tree automata"@en . "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 o"@en . "Bouajjani, Ahmed" . . "26230" . . "Abstract Regular (Tree) Model Checking"@en . "Rogalewicz, Adam" . "4"^^ . . "[4475F77B56FE]" . . "2"^^ . "Abstract Regular (Tree) Model Checking" . . . "1433-2779" . . . "2" . .