Split Transition Power Abstraction for Unbounded Safety

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Split Transition Power Abstraction for Unbounded Safety

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Split Transition Power Abstraction for Unbounded Safety

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

<a href="/cs/project/GA20-07487S" target="_blank" >GA20-07487S: Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů</a><br>

Návaznosti

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

Rok uplatnění

2022

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

Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022

ISBN

978-3-85448-053-2

ISSN

—

e-ISSN

—

Počet stran výsledku

10

Strana od-do

349-358

Název nakladatele

TU Wien Academic Press

Místo vydání

Vídeň

Místo konání akce

Trento, Italy

Datum konání akce

17. 10. 2022

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

WRD - Celosvětová akce

Kód UT WoS článku

—