Farkas-Based Tree Interpolation

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F20%3A10421780" target="_blank" >RIV/00216208:11320/20:10421780 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-65474-0_16" target="_blank" >https://doi.org/10.1007/978-3-030-65474-0_16</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-65474-0_16" target="_blank" >10.1007/978-3-030-65474-0_16</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Farkas-Based Tree Interpolation

Popis výsledku v původním jazyce

Linear arithmetic over reals (LRA) underlies a wide range of SMT-based modeling approaches, and, strengthened with Craig interpolation using Farkas&apos; 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.

Název v anglickém jazyce

Farkas-Based Tree Interpolation

Popis výsledku anglicky

Linear arithmetic over reals (LRA) underlies a wide range of SMT-based modeling approaches, and, strengthened with Craig interpolation using Farkas&apos; 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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA20-07487S" target="_blank" >GA20-07487S: Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2020

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Static Analysis

ISBN

978-3-030-65473-3

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

23

Strana od-do

357-379

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Chicago, United States (Online)

Datum konání akce

18. 11. 2020

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000728160300016