Transition Power Abstractions for Deep Counterexample Detection

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F22%3A10455349" target="_blank" >RIV/00216208:11320/22:10455349 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-99524-9_29" target="_blank" >https://doi.org/10.1007/978-3-030-99524-9_29</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-99524-9_29" target="_blank" >10.1007/978-3-030-99524-9_29</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Transition Power Abstractions for Deep Counterexample Detection

Popis výsledku v původním jazyce

While model checking safety of infinite-state systems by inferring state invariants has steadily improved recently, most verification tools still rely on a technique based on bounded model checking to detect safety violations. In particular, the current techniques typically analyze executions by unfolding transitions one step at a time, and the slow growth of execution length prevents detection of deep counterexamples before the tool reaches its limits on computations. We propose a novel model-checking algorithm that is capable of both proving unbounded safety and finding long counterexamples. The idea is to use Craig interpolation to guide the creation of symbolic abstractions of exponentially longer sequences of transitions. Our experimental analysis shows that on unsafe benchmarks with deep counterexamples our implementation can detect faulty executions that are at least an order of magnitude longer than those detectable by the state-of-the-art tools.

Název v anglickém jazyce

Transition Power Abstractions for Deep Counterexample Detection

Popis výsledku anglicky

While model checking safety of infinite-state systems by inferring state invariants has steadily improved recently, most verification tools still rely on a technique based on bounded model checking to detect safety violations. In particular, the current techniques typically analyze executions by unfolding transitions one step at a time, and the slow growth of execution length prevents detection of deep counterexamples before the tool reaches its limits on computations. We propose a novel model-checking algorithm that is capable of both proving unbounded safety and finding long counterexamples. The idea is to use Craig interpolation to guide the creation of symbolic abstractions of exponentially longer sequences of transitions. Our experimental analysis shows that on unsafe benchmarks with deep counterexamples our implementation can detect faulty executions that are at least an order of magnitude longer than those detectable by the state-of-the-art tools.

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

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I

ISBN

978-3-030-99523-2

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

19

Strana od-do

524-542

Název nakladatele

SPRINGER INTERNATIONAL PUBLISHING AG

Místo vydání

CHAM

Místo konání akce

Munich

Datum konání akce

2. 4. 2022

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

WRD - Celosvětová akce

Kód UT WoS článku

000782396700029