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...
Main Authors: | , |
---|---|
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 |