Periplo: a framework for producing effective interpolants in SAT-based software verification Propositional interpolation is widely used as a means of overapproximation to achieve efficient SAT-based symbolic model checking. Different verification applications exploit interpolants for different purposes; it is unlikely that a single interpolation procedure could provide interpolants fit for all cases. This paper describes the PeRIPLO framework, an interpolating SAT-solver that implements a set of techniques to generate and manipulate interpolants for different model checking tasks. We demonstrate the flexibility of the framework in two software bounded model checking applications: verification of a given source code incrementally with respect to various properties, and verification of software upgrades with respect to a fixed set of properties. Both applications use interpolation for generating function summaries. Our systematic experimental investigation shows that size and logical strength of interpolants significantly affect verification, that these characteristics depend on the role played by interpolants, and that therefore techniques for tuning size and strength can be used to customize interpolants in different applications.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Jančík, Pavel; Kofroň, Jan; Alt, Leonardo; Fedyukovich, Grigory; Hyvärinen, Antti E. J.; Sharygina, Natasha: Exploiting partial variable assignment in interpolation-based model checking (2019)
- Hyvärinen, Antti E. J.; Marescotti, Matteo; Alt, Leonardo; Sharygina, Natasha: Opensmt2: an SMT solver for multi-core and cloud computing (2016)
- Leroux, Jérôme; Rümmer, Philipp; Subotić, Pavle: Guiding Craig interpolation with domain-specific abstractions (2016)
- Schlaipfer, Matthias; Weissenbacher, Georg: Labelled interpolation systems for hyper-resolution, clausal, and local proofs (2016)
- Fedyukovich, Grigory; Sharygina, Natasha: Towards completeness in bounded model checking through automatic recursion depth detection (2015)
- Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei: Resolution proof transformation for compression and interpolation (2014)
- Rollini, Simone Fulvio; Alt, Leonardo; Fedyukovich, Grigory; Hyvärinen, Antti E. J.; Sharygina, Natasha: PeRIPLO: a framework for producing effective interpolants in SAT-based software verification (2013)