Farkas-Based Tree Interpolation
| Autor: | Grigory Fedyukovich, Antti E. J. Hyvärinen, Martin Blicha, Sepideh Asadi, Natasha Sharygina |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Lemma (mathematics)
Computer science ComputingMethodologies_IMAGEPROCESSINGANDCOMPUTERVISION MathematicsofComputing_NUMERICALANALYSIS 020207 software engineering Craig interpolation 02 engineering and technology Set (abstract data type) Tree (data structure) Range (mathematics) Tree structure Fragment (logic) ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Algorithm ComputingMethodologies_COMPUTERGRAPHICS Interpolation |
| Zdroj: | Static Analysis ISBN: 9783030654733 SAS |
| DOI: | 10.1007/978-3-030-65474-0_16 |
| Popis: | Linear arithmetic over reals (LRA) underlies a wide range of SMT-based modeling approaches, and, strengthened with Craig interpolation using Farkas’ lemma, is a central tool for efficient over-approximation. Recent advances in LRA interpolation have resulted in a range of promising interpolation algorithms with so far poorly understood properties. In this work we study the Farkas-based algorithms with respect to tree interpolation, a practically important approach where a set of interpolants is constructed following a given tree structure. We classify the algorithms based on whether they guarantee the tree interpolation property, and present how to lift a recently introduced approach producing conjunctive LRA interpolants to tree interpolation in the quantifier-free LRA fragment of first-order logic. Our experiments show that the standard interpolation and the approach using conjunctive interpolants are complementary in tree interpolation, and suggest that their combination would be very powerful in practice. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|