Instantiation-Based Interpolation for Quantified Formulae in CSIsat

The paper describes an implementation of instantiation-based Craig interpolation for quantified formulae. The implementation is based on the CSIsat interpolating solver. The tool supports interpolation for formulae with linear real arithmetic, uninterpreted functions and quantifiers. The paper sugge...

Full description

Bibliographic Details
Main Authors: Vadim Mutilin, Mikhail Mandrykin
Format: Article
Language:English
Published: Ivannikov Institute for System Programming of the Russian Academy of Sciences 2018-10-01
Series:Труды Института системного программирования РАН
Subjects:
Online Access:https://ispranproceedings.elpub.ru/jour/article/view/1016
id doaj-80e7cfc3cb044be9a8dcb938368d61c4
record_format Article
spelling doaj-80e7cfc3cb044be9a8dcb938368d61c42020-11-25T01:56:25Zeng Ivannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-012201016Instantiation-Based Interpolation for Quantified Formulae in CSIsatVadim Mutilin0Mikhail Mandrykin1ИСП РАНИСП РАНThe paper describes an implementation of instantiation-based Craig interpolation for quantified formulae. The implementation is based on the CSIsat interpolating solver. The tool supports interpolation for formulae with linear real arithmetic, uninterpreted functions and quantifiers. The paper suggests usage of an external decision procedure (namely CVC3) for quantified formula instantiation. It describes how the CSIsat and CVC3 tools were modified in order to support quantified formulae interpolation. The paper also contains results for benchmarking the modified CSIsat tool on a set of tests obtained by randomly splitting tasks from the SMTLIB library as well as on a small collection of specific dedicated interpolation tasks generated by encoding several manually specified parameterized error trace patterns with quantified logical formulae. The approach to interpolation considered in the paper is based on the recently proposed extension of the McMillan’s algorithm for resolution-based interpolant generation that was suggested earlier for implementation in the SMTInterpol interpolating solver by its developers. The extended algorithm additionally requires a set of quantified subformula instances sufficient for unsatisfiability proof of the initial formula and produces possibly quantified interpolants. A proper implementation of the algorithm could potentially be used in predicate abstraction-based verification tools for obtaining abstraction predicates from counterexamples by Craig interpolation. Though the evaluation presented in the paper showed that the considered implementation turned out to be too inefficient for this purpose due to significant repetitive proof overhead, which arose from combining a more efficient and advanced solver with a significantly less efficient one (in CVC3+CSIsat combination CSIsat is much less efficient than CVC3).https://ispranproceedings.elpub.ru/jour/article/view/1016интерполяцияинтерполянт крейгакванторыинстанцированиерешательаксиомы
collection DOAJ
language English
format Article
sources DOAJ
author Vadim Mutilin
Mikhail Mandrykin
spellingShingle Vadim Mutilin
Mikhail Mandrykin
Instantiation-Based Interpolation for Quantified Formulae in CSIsat
Труды Института системного программирования РАН
интерполяция
интерполянт крейга
кванторы
инстанцирование
решатель
аксиомы
author_facet Vadim Mutilin
Mikhail Mandrykin
author_sort Vadim Mutilin
title Instantiation-Based Interpolation for Quantified Formulae in CSIsat
title_short Instantiation-Based Interpolation for Quantified Formulae in CSIsat
title_full Instantiation-Based Interpolation for Quantified Formulae in CSIsat
title_fullStr Instantiation-Based Interpolation for Quantified Formulae in CSIsat
title_full_unstemmed Instantiation-Based Interpolation for Quantified Formulae in CSIsat
title_sort instantiation-based interpolation for quantified formulae in csisat
publisher Ivannikov Institute for System Programming of the Russian Academy of Sciences
series Труды Института системного программирования РАН
issn 2079-8156
2220-6426
publishDate 2018-10-01
description The paper describes an implementation of instantiation-based Craig interpolation for quantified formulae. The implementation is based on the CSIsat interpolating solver. The tool supports interpolation for formulae with linear real arithmetic, uninterpreted functions and quantifiers. The paper suggests usage of an external decision procedure (namely CVC3) for quantified formula instantiation. It describes how the CSIsat and CVC3 tools were modified in order to support quantified formulae interpolation. The paper also contains results for benchmarking the modified CSIsat tool on a set of tests obtained by randomly splitting tasks from the SMTLIB library as well as on a small collection of specific dedicated interpolation tasks generated by encoding several manually specified parameterized error trace patterns with quantified logical formulae. The approach to interpolation considered in the paper is based on the recently proposed extension of the McMillan’s algorithm for resolution-based interpolant generation that was suggested earlier for implementation in the SMTInterpol interpolating solver by its developers. The extended algorithm additionally requires a set of quantified subformula instances sufficient for unsatisfiability proof of the initial formula and produces possibly quantified interpolants. A proper implementation of the algorithm could potentially be used in predicate abstraction-based verification tools for obtaining abstraction predicates from counterexamples by Craig interpolation. Though the evaluation presented in the paper showed that the considered implementation turned out to be too inefficient for this purpose due to significant repetitive proof overhead, which arose from combining a more efficient and advanced solver with a significantly less efficient one (in CVC3+CSIsat combination CSIsat is much less efficient than CVC3).
topic интерполяция
интерполянт крейга
кванторы
инстанцирование
решатель
аксиомы
url https://ispranproceedings.elpub.ru/jour/article/view/1016
work_keys_str_mv AT vadimmutilin instantiationbasedinterpolationforquantifiedformulaeincsisat
AT mikhailmandrykin instantiationbasedinterpolationforquantifiedformulaeincsisat
_version_ 1724980354971860992