D 2014

Context-Switch-Directed Verification in DIVINE

ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT

Základní údaje

Originální název

Context-Switch-Directed Verification in DIVINE

Autoři

ŠTILL, Vladimír (203 Česká republika, garant, domácí), Petr ROČKAI (703 Slovensko, domácí) a Jiří BARNAT (203 Česká republika, domácí)

Vydání

Neuveden, Mathematical and Engineering Methods in Computer Science, od s. 135-146, 12 s. 2014

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/14:00084599

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-14895-3

ISSN

DOI

UT WoS

000357573300012

Klíčová slova anglicky

model checking; LLVM; context-switch bounded verification

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 9. 11. 2015 12:23, RNDr. Vladimír Štill, Ph.D.

Anotace

V originále

In model checking of real-life C and C++ programs, both search efficiency and counterexample readability are very important. In this paper, we suggest context-switch-directed exploration as a way to find a well-readable counterexample faster. Furthermore, we allow to limit the number of context switches used in state-space exploration if desired. The new algorithm is implemented in the DIVINE model checker and enables both unbounded and bounded context-switch-directed exploration for models given in LLVM bitcode, which efficiently allows for verification of multi-threaded C and C++ programs.

Návaznosti

MUNI/A/0855/2013, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty