Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GA14-11384S" target="_blank" >GA14-11384S: Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Computer Aided Verification
ISBN
978-3-319-41527-7
ISSN
0302-9743
e-ISSN
—
Number of pages
21
Pages from-to
271-291
Publisher name
Springer International Publishing
Place of publication
Germany
Event location
Toronto, Kanada
Event date
Jul 17, 2016
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000387731200015