Farkas-Based Tree Interpolation

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Farkas-Based Tree Interpolation

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/GA20-07487S" target="_blank" >GA20-07487S: Scalable Techniques for Analysis of Complex Properties of Computer Systems</a><br>

Continuities

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

Publication year

2020

Confidentiality

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

Article name in the collection

Static Analysis

ISBN

978-3-030-65473-3

ISSN

0302-9743

e-ISSN

—

Number of pages

23

Pages from-to

357-379

Publisher name

Springer

Place of publication

Cham

Event location

Chicago, United States (Online)

Event date

Nov 18, 2020

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000728160300016