Abstract
We show how model checking procedures for different kinds of infinite-state systems can be formalized as a generic constraint-solving procedure, viz. the saturation under a parametric set of inference rules. The procedures can be classified by the solved form they are to compute. This solved form is a recursive (automaton-like) definition of the set of states satisfying the given temporal property in the case of systems over stacks or other symbolic data. © Springer-Verlag Berlin Heidelberg 2000.
Cite
CITATION STYLE
Podelski, A. (2000). Model checking as constraint solving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1824 LNCS, pp. 22–37). Springer Verlag. https://doi.org/10.1007/978-3-540-45099-3_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
