an Interpolating SMT Solver
About SMTInterpol
SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. The solver is developed at the Chair of Software Engineering at the University of Freiburg.
The solver is written in Java and can be used on any operating system that supports Java Version 6.
The solver reads input in SMTLIB Version 2 format.
The current version of SMTInterpol is 2.0. It supports interpolation for the combination of the quantifier-free fragments of the theories of uninterpreted functions, linear real arithmetic, and linear integer arithmetic.
System Requirements
SMTInterpol needs a Java 6 JRE. No special hardware is necessary but depending on the input problem, a fast CPU and a good amount of RAM might be useful.
SMTInterpol is developed by Jochen Hoenicke, J├╝rgen Christ, and Alexander Nutz in the context of the AVACS (Automatic Verification and Analysis of Complex Systems) project. If you have any questions, suggestions, or if you want to contribute, feel free to contact us.
SMTInterpol is distributed under LGPL Version 3.
SMTInterpol in Action
SMTInterpol participates in the SMT-COMP 2012. See this page or the news page for further details.
Further Development
We plan to extend SMTInterpol to reason about arrays and quantifiers. Interpolation procedures for these logics will be the next big challenge. Additionally, we try to add more flexibility to our interpolation engine to enable model checkers to easily adjust the interpolation procedure of SMTInterpol to their needs.

Last modified: Tue Dec 17 15:08:58 CET 2013   Valid XHTML 1.0 TransitionalValid CSS!