Instantiation-Based Interpolation for Quantified Formulae in CSIsat.
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.Полный текст статьи в формате pdf (на английском)
Proceedings of the 6th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), pp. 85-93.