Model Checking of C and C++ with DIVINE 4

D 2017

Model Checking of C and C++ with DIVINE 4

BARANOVÁ, Zuzana; Jiří BARNAT; Katarína KEJSTOVÁ; Tadeáš KUČERA; Henrich LAUKO et al.

Základní údaje

Originální název

Model Checking of C and C++ with DIVINE 4

Autoři

BARANOVÁ, Zuzana; Jiří BARNAT; Katarína KEJSTOVÁ; Tadeáš KUČERA; Henrich LAUKO; Jan MRÁZEK; Petr ROČKAI a Vladimír ŠTILL

Vydání

Cham, Automated Technology for Verification and Analysis, od s. 201-207, 7 s. 2017

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"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/17:00095126

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-68166-5

ISSN

Klíčová slova anglicky

Model Checking; Verification; C; C++; DIVINE

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 1. 10. 2018 16:24, prof. RNDr. Jiří Barnat, Ph.D.

Anotace

V originále

The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.

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/0897/2016, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/0992/2016, 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

Citovat

BARANOVÁ, Zuzana; Jiří BARNAT; Katarína KEJSTOVÁ; Tadeáš KUČERA; Henrich LAUKO; Jan MRÁZEK; Petr ROČKAI a Vladimír ŠTILL. Model Checking of C and C++ with DIVINE 4. In Deepak D'Souza, K. Narayan Kumar. Automated Technology for Verification and Analysis. Cham: Springer International Publishing, 2017, s. 201-207. ISBN 978-3-319-68166-5. Dostupné z: https://doi.org/10.1007/978-3-319-68167-2_14.

@inproceedings{1394153,
   author = {Baranová, Zuzana and Barnat, Jiří and Kejstová, Katarína and Kučera, Tadeáš and Lauko, Henrich and Mrázek, Jan and Ročkai, Petr and Štill, Vladimír},
   address = {Cham},
   booktitle = {Automated Technology for Verification and Analysis},
   doi = {https://doi.org/10.1007/978-3-319-68167-2_14},
   editor = {Deepak D'Souza, K. Narayan Kumar},
   keywords = {Model Checking; Verification; C; C++; DIVINE},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-319-68166-5},
   pages = {201-207},
   publisher = {Springer International Publishing},
   title = {Model Checking of C and C++ with DIVINE 4},
   url = {https://link.springer.com/chapter/10.1007/978-3-319-68167-2_14},
   year = {2017}
}

TY  - CONF
ID  - 1394153
AU  - Baranová, Zuzana - Barnat, Jiří - Kejstová, Katarína - Kučera, Tadeáš - Lauko, Henrich - Mrázek, Jan - Ročkai, Petr - Štill, Vladimír
PY  - 2017
TI  - Model Checking of C and C++ with DIVINE 4
PB  - Springer International Publishing
CY  - Cham
SN  - 9783319681665
KW  - Model Checking
KW  - Verification
KW  - C
KW  - C++
KW  - DIVINE
UR  - https://link.springer.com/chapter/10.1007/978-3-319-68167-2_14
L2  - https://link.springer.com/chapter/10.1007/978-3-319-68167-2_14
N2  - The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.
ER  -

BARANOVÁ, Zuzana; Jiří BARNAT; Katarína KEJSTOVÁ; Tadeáš KUČERA; Henrich LAUKO; Jan MRÁZEK; Petr ROČKAI a Vladimír ŠTILL. Model Checking of C and C++ with DIVINE 4. In Deepak D'Souza, K. Narayan Kumar. \textit{Automated Technology for Verification and Analysis}. Cham: Springer International Publishing, 2017, s.~201-207. ISBN~978-3-319-68166-5. Dostupné z: https://doi.org/10.1007/978-3-319-68167-2\_{}14.

Přehled o publikaci