About SMTInterpol
The solver is written
in
Java
and can be used on any operating system that supports Java Version
6 or above.
Status
The current version of SMTInterpol supports interpolation for the
combination of the quantifier-free fragments of the theories of
uninterpreted functions, linear real arithmetic, linear integer
arithmetic, and arrays.
System Requirements
SMTInterpol needs a Java 6 JRE or above. 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 and
Tanja
Schindler in the context of the SIGSMCAP
(SMT-based Interpolant Generation
for Software ModelChecking of Array Programs) project, and by
Alexander Nutz.
If you have any questions, suggestions,
or if you want to contribute, feel free to contact us.
Previous contributors include
Jürgen Christ.
Bug Reports
License
SMTInterpol is distributed under LGPL Version 3.
SMTInterpol in Action
SMTInterpol participates regularly in the
SMT-COMP. See this page or
the news page for further details.
Last modified: Mon Feb 26 18:57:17 CET 2018 
