-
Patrick Cousot.
Refining Model Checking by Abstract Interpretation (Invited Seminar)
Seminario, Gio. Sep. 24, 1998, Università degli Studi di Udine.
- Abstract:
Formal methods combining abstract interpretation and model-checking have
been considered to cope with the high complexity of very large systems and
the undecidability problems for infinite state systems. Consequently, all
properties of all systems cannot be automatically verified in finite or
reasonable time. Some form of approximation has to be considered.
In abstract model-checking, the semantics of an infinite
transition system is abstracted to get a finite approximation on which
temporal-logic/µ-calculus model-checking can be directly applied.
Two improvements of abstract model-checking are proposed which
can be applied to infinite abstract transition systems:
- A new combination of forwards and backwards abstract fixed-point
model-checking computations for universal safety. It computes a more
precise result than that computed by conjunction of the forward and
backward analyses alone, without needing to refine the abstraction;
- When abstraction is unsound (as can happen in minimum/maximum
path-length problems), it is proposed to use the partial results of a
classical combination of forward and backward abstract interpretation
analyses for universal safety in order to reduce, on-the-fly, the
concrete state space to be searched by model-checking.
- Slides: .pdf.
- Reference: