PeRIPLO

Note: PeRIPLO functionality is now implemented in OpenSMT2 and is better maintained there.

PeRIPLO is an open-source SAT-solver that features resolution proof manipulation and interpolant generation capabilities. The acronym stands for Proof tRansformer and Interpolator for Propositional Logic.

PeRIPLO, written in C++ and built on top of MiniSAT 2.2.0 (http://minisat.se), was born from OpenSMT to provide specific support for SAT-based model checking in FunFrog and eVolCheck.

PeRIPLO offers support for the following tasks:

  • SAT-solving and proof logging
  • Resolution proof compression and transformation
  • Interpolant generation by means of the Labeled Interpolation System
  • Generation of sequences of interpolants for Path Interpolation, Simultaneous Abstraction, State-Transition interpolation, Tree Interpolation

PeRIPLO is currently released under the GNU General Public Licence version 3. The tool can be downloaded here. A tutorial on how to use PeRIPLO can be found here.

Comments, suggestions and requests are very welcome at sepideh.asadi [at] usi.ch .

 

Published papers:

  1. PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification, Rollini, S.F., Alt L., Fedyukovich G., Hyvaerinen A., and Sharygina N. , Logic for Programming Artificial Intelligence and Reasoning (LPAR), Stellenbosch, South Africa, 2013