Split Transition Power Abstraction for Unbounded Safety
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F22%3A10455358" target="_blank" >RIV/00216208:11320/22:10455358 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_42" target="_blank" >https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_42</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.34727/2022/isbn.978-3-85448-053-2_42" target="_blank" >10.34727/2022/isbn.978-3-85448-053-2_42</a>
Alternative languages
Result language
angličtina
Original language name
Split Transition Power Abstraction for Unbounded Safety
Original language description
Transition Power Abstraction (TPA) is a recent symbolic model checking approach that leverages Craig interpolation to create a sequence of symbolic abstractions for transition paths that double in length with each new element. This doubling abstraction allows the approach to find bugs that require long executions much faster than traditional approaches that unfold transitions one at a time, but its ability to prove system safety is limited. This paper proposes a novel instantiation of the TPA approach capable of proving unbounded safety efficiently while preserving the unique capability to detect deep counterexamples. The idea is to split the transition over-approximations in two complementary parts. One part focuses only on reachability in fixed number of steps, the second part complements it by summarizing all shorter paths. The resulting split abstractions are suitable for discovering safe transition invariants, making the SPLIT-TPA approach much more efficient in proving safety and even improving the counterexample detection. The approach is implemented in the constrained Horn clause solver GOLEM and our experimental comparison against state-of-the-art solvers shows it to be both competitive and complementary.
Czech name
—
Czech description
—
Classification
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)
Result continuities
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)
Others
Publication year
2022
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
Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022
ISBN
978-3-85448-053-2
ISSN
—
e-ISSN
—
Number of pages
10
Pages from-to
349-358
Publisher name
TU Wien Academic Press
Place of publication
Vídeň
Event location
Trento, Italy
Event date
Oct 17, 2022
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—