Model checking as constraint solving
| Author(s) : | Andreas Podelski, |
| Publisher : | N/A |
| Publication Date : | 2000 |
| ISSN : | N/A |
| Abstract : | Abstract. We show how model checking procedures for dierent kinds of innite-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 classied by the solved form they are to compute. This solved form is a recursive (automaton-like) denition of the set of states satisfying the given temporal property in the case of systems over stacks or other symbolic data., |