Refining Model Checking by Abstract Interpretation

Patrick COUSOT


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/$\mu$-calculus model-checking can be directly applied.

Two improvements of abstract model-checking are proposed which can be applied to infinite abstract transition systems:



Surveys on model checking: