×

zbMATH — the first resource for mathematics

Infinite state model checking by abstract interpretation and program specialisation. (English) Zbl 0964.68086
Bossi, Annalisa (ed.), Logic-based program synthesis and transformation. 9th international workshop, LOPSTR ’99. Venice, Italy, September 22-24, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1817, 62-81 (2000).
Summary: We illustrate the use of logic programming techniques for finite model checking of CTL formulae. We present a technique for infinite state model checking of safety properties based upon logic program specialisation and analysis techniques. The power of the approach is illustrated on several examples. For that, the efficient tools LOGEN and ECCE are used. We discuss how this approach has to be extended to handle more complicated infinite state systems and to handle arbitrary CTL formulae.
For the entire collection see [Zbl 0941.00033].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N17 Logic programming
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
ECCE; LOGEN; XSB
PDF BibTeX XML Cite