SMTInterpol: An Interpolating SMT Solver

Abstract. Craig interpolation is an active research topic and has become a powerful technique in verification. We present SMTInterpol, an interpolating SMT solver for the quantifier-free fragment of the combination of the theory of uninterpreted functions and the theory of linear arithmetic over integers and reals. SMTInterpol is SMTLIB 2 compliant and available under an open source software license (LGPL v3).

• Type: Journal
• Year: 2012
• Where: SPIN
• Authors: Jürgen Christ, Jochen Hoenicke, Alexander Nutz
• Keywords: Free Fragment, Linear Arithmetic, SPIN 2012, Theoretical Computer Science, Uninterpreted Functions