PeRIPLO is our most recent tool, 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 (, 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 rollinis at .