PeRIPLO
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 (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 rollinis at usi.ch .
The Lab is funded by Swiss National Science Foundation, Foundation Tasso, Hasler Foundation, EU-COST initiative and EU FP7/Pincette.
