D 2013

DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs

BARNAT, Jiří, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK, Jan KRIHO et. al.

Základní údaje

Originální název

DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs

Název česky

DiVinE 3.0 -- Explicitně-stavový nástroj pro ověřování modelu pro vícevláknové C a C++ programy

Autoři

BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí), Vojtěch HAVEL (203 Česká republika, domácí), Jan HAVLÍČEK (203 Česká republika, domácí), Jan KRIHO (203 Česká republika, domácí), Milan LENČO (703 Slovensko, domácí), Petr ROČKAI (703 Slovensko, domácí), Vladimír ŠTILL (203 Česká republika, domácí) a Jiří WEISER (203 Česká republika, domácí)

Vydání

Heidelberg, Computer Aided Verification 2013, od s. 863-868, 6 s. 2013

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

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/13:00066526

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-39798-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-39799-8_60

Klíčová slova anglicky

model checking; LLVM; C++; C; LTL; timed automata

Štítky

core_A, firank_1
Změněno: 27. 4. 2014 23:39, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We present a new release of the parallel and distributed LTL model checker DIVINE. The major improvements in this new release is an extension of the class of systems that may be verified with the model checker, while preserving the unique DIVINE feature, namely parallel and distributed-memory processing. Version 3.0 comes with support for direct model checking of (closed) multithreaded C/C++ programs, full untimed-LTL model checking of timed automata, and a general-purpose framework for interfacing with arbitrary system modelling tools.

Návaznosti

GAP202/11/0312, projekt VaV
Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)
Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
MUNI/A/0739/2012, interní kód MU
Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
Zobrazeno: 10. 11. 2024 21:53