Lars Helander

Implementation and Evaluation of an Interpolation Based Model Checker

Abstract

A Craig interpolant C of an unsatisfiable formula A & B is a formula over the common variables of A and B such that (1) A implies C and (2) C is inconsistent with B. The existence of C is guaranteed in the context of propositional logic.

 

In this Master’s thesis, a complete interpolation and SAT-based symbolic model checking algorithm is described. The algorithm uses resolution refutations of unsatisfiable bounded model checking instances to compute Craig interpolants that can be used as over-approximations of the traditional image operator used in symbolic reachability analysis.

 

As part of the Master’s thesis, the interpolation based algorithm has been implemented and evaluated. The report includes benchmarks from the implementation, and it is shown that it compares favorably to traditional methods on many instances.

 

Additionally, using saturation in combination with the interpolation based algorithm is shown to reduce the run time by one or two orders of magnitude on many benchmarks. This is probably the first time saturation and interpolation based model checking has been combined.

Implementering och utvärdering av en interpolationsbaserad model checker

Sammanfattning

En Craig interpolant C för en osatisfierbar formel A & B är en formel över de gemensamma variablerna för A och B sådan att (1) A medför C och (2) C motsäger B. C:s existens är garanterad när A och B är satslogiska formler.

 

I detta examensarbete ges en beskrivning av en komplett interpolations- och SAT-baserad model checking algoritm. Algoritmen använder resolutionsbevis för osatisfierbara probleminstanser av bounded model checking för att beräkna Craig interpolanter som kan användas som över-approximationer av den traditionella image-operatorn som används i symbolisk reachability analysis.

 

Som en del av examensarbetet har den interpolationsbaserade algoritmen implementerats och utvärderats. Denna rapport innehåller benchmarks som visar att interpolationsmetoden är jämförelsevis bättre än traditionella metoder på många exempel.

 

Till yttermera visso visas att mättning i kombination med den interpolationsbaserade algoritmen reducerar körtiden en eller två tiopotenser på många benchmarks. Detta är troligen första gången mättning och interpolationsbaserad model checking har kombinerats.