Decomposing Farkas Interpolants

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F19%3A10397044" target="_blank" >RIV/00216208:11320/19:10397044 - isvavai.cz</a>

Result on the web

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

DOI - Digital Object Identifier

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

Result language

angličtina

Original language name

Decomposing Farkas Interpolants

Original language description

Modern verification commonly models software with Boolean logic and a system of linear inequalities over reals and over-approximates the reachable states of the model with Craig interpolation to obtain, for example, candidates for inductive invariants. Interpolants for the linear system can be efficiently constructed from a Simplex refutation by applying the Farkas&apos; lemma. However, Farkas interpolants do not always suit the verification task and in the worst case they may even be the cause of divergence of the verification algorithm. This work introduces the decomposed interpolants, a fundamental extension of the Farkas interpolants obtained by identifying and separating independent components from the interpolant structure using methods from linear algebra. We integrate our approach to the model checker Sally and show experimentally that a portfolio of decomposed interpolants results in immediate convergence on instances where state-of-the-art approaches diverge. Being based on the efficient Simplex method, the approach is very competitive also outside these diverging cases.

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/GA17-12465S" target="_blank" >GA17-12465S: Verification and Bug Hunting for Advanced Software</a><br>

Continuities

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

Publication year

2019

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

TACAS 2019: Tools and Algorithms for the Construction and Analysis of Systems

ISBN

978-3-030-17461-3

ISSN

0302-9743

e-ISSN

—

Number of pages

18

Pages from-to

3-20

Publisher name

Springer

Place of publication

Cham

Event location

Praha

Event date

Apr 6, 2019

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—