Ivannikov Institute for System Programming of the RAS


Instantiation-Based Interpolation for Quantified Formulae in CSIsat.

Authors

Mutilin V., Mandrykin M.

Abstract

The paper describes an implementation of instantiation-based interpolation for quantified formulae in modified CSIsat tool. The tool supports interpolation for formulae with linear real arithmetic, uninterpreted functions and quantifiers. We propose in this paper using external SMT-solver CVC3 for quantified expressions instantiation, then we describe how we modified CSIsat and CVC3 tools in order to support quantified formulae interpolation. We also present results of benchmarking the modified CSIsat tool on SMTLIB test set as well as on our specially generated interpolation tasks.

Full text of the paper in pdf

Keywords

interpolation, Craig interpolant, quantifiers, instantiation, solver, axioms.

Edition

Proceedings of the 6th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), pp. 85-93.

DOI: 10.15514/SYRCOSE-2012-6-12

Research Group

All publications during 2012 All publications