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.
Status
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.
Team
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.
License
SMTInterpol is distributed under LGPL Version 3.
SMTInterpol in Action
SMTInterpol participated in the SMT-COMP 2011 in the main and in the application track.
See these pages 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 May 15 16:35:28 CEST 2012
