Transition Power Abstractions for Deep Counterexample Detection

Result code in 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>

Result on the web

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

Result language

angličtina

Original language name

Transition Power Abstractions for Deep Counterexample Detection

Original language description

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.

Czech name

—

Czech description

—

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)

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)

Publication year

2022

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

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

Number of pages

19

Pages from-to

524-542

Publisher name

SPRINGER INTERNATIONAL PUBLISHING AG

Place of publication

CHAM

Event location

Munich

Event date

Apr 2, 2022

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000782396700029