DIVINE: Explicit-State LTL Model Checker

ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. DIVINE: Explicit-State LTL Model Checker. In M. Chechik and J.-F. Raskin. Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. New York, NY, USA: Springer-Verlag New York, Inc., 2016, s. 920-922. ISBN 978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9_60.

Základní údaje

Originální název

DIVINE: Explicit-State LTL Model Checker

Autoři

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

Vydání

New York, NY, USA, Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, od s. 920-922, 3 s. 2016

Nakladatel

Springer-Verlag New York, Inc.

---

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"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088093

Organizační jednotka

Fakulta informatiky

ISBN

978-3-662-49673-2

ISSN

DOI

http://dx.doi.org/10.1007/978-3-662-49674-9_60

UT WoS

000406428000060

Klíčová slova anglicky

DIVINE model checker; LTL model checking

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

DIVINE is an LLVM-based LTL model checker that follows the standard automata-based approach to explicit-state model checking. It aims at verification of unmodified parallel C & C++ programs without inputs. To achieve this DIVINE employs several reduction techniques combined with high-performance parallel and distributed computing.

---

Návaznosti

GA15-08772S, projekt VaV	Název: Analýza korektnosti vícevláknových programů v C a C++ Investor: Grantová agentura ČR, Correctness Analysis of C and C++ Programs with Threads
MUNI/A/0935/2015, 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
MUNI/A/0945/2015, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V. Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty