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
Comments, suggestions and requests are very welcome at sepideh.asadi [at] usi.ch .
- PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification, , Logic for Programming Artificial Intelligence and Reasoning (LPAR), Stellenbosch, South Africa, 2013