Infinite-state liveness-to-safety via implicit abstraction and well-founded relations

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F16%3A10323243" target="_blank" >RIV/00216208:11320/16:10323243 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007%2F978-3-319-41528-4_15" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-319-41528-4_15</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-41528-4_15" target="_blank" >10.1007/978-3-319-41528-4_15</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Infinite-state liveness-to-safety via implicit abstraction and well-founded relations

Popis výsledku v původním jazyce

We present a fully symbolic LTL model checking approach for infinite-state transition systems. We extend liveness-to-safety, a prominent approach in the finite-state case, by means of implicit abstraction, to effectively prove the absence of abstract fair loops without explicitly constructing the abstract state space. We increase the effectiveness of the approach by integrating termination techniques based on well-founded relations derived from ranking functions. The idea is to prove that any existing abstract fair loop is covered by a given set of well-founded relations. Within this framework, K-liveness is integrated as a generic ranking function. The algorithm iterates by attempting to remove spurious abstract fair loops: either it finds new predicates, to avoid spurious abstract prefixes, or it introduces new well-founded relations, based on the analysis of the abstract lasso. The implementation fully leverages the efficiency and incrementality of the underlying safety checker IC3ia. The proposed approach outperforms other tools on a wide class of benchmarks.

Název v anglickém jazyce

Infinite-state liveness-to-safety via implicit abstraction and well-founded relations

Popis výsledku anglicky

We present a fully symbolic LTL model checking approach for infinite-state transition systems. We extend liveness-to-safety, a prominent approach in the finite-state case, by means of implicit abstraction, to effectively prove the absence of abstract fair loops without explicitly constructing the abstract state space. We increase the effectiveness of the approach by integrating termination techniques based on well-founded relations derived from ranking functions. The idea is to prove that any existing abstract fair loop is covered by a given set of well-founded relations. Within this framework, K-liveness is integrated as a generic ranking function. The algorithm iterates by attempting to remove spurious abstract fair loops: either it finds new predicates, to avoid spurious abstract prefixes, or it introduces new well-founded relations, based on the analysis of the abstract lasso. The implementation fully leverages the efficiency and incrementality of the underlying safety checker IC3ia. The proposed approach outperforms other tools on a wide class of benchmarks.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA14-11384S" target="_blank" >GA14-11384S: Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí</a><br>

Návaznosti

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

Rok uplatnění

2016

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

Computer Aided Verification

ISBN

978-3-319-41527-7

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

21

Strana od-do

271-291

Název nakladatele

Springer International Publishing

Místo vydání

Germany

Místo konání akce

Toronto, Kanada

Datum konání akce

17. 7. 2016

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

WRD - Celosvětová akce

Kód UT WoS článku

000387731200015