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. doi:10.1007/978-3-319-68167-2_14.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Model Checking of C and C++ with DIVINE 4
Autoři BARANOVÁ, Zuzana (703 Slovensko, domácí), Jiří BARNAT (203 Česká republika, garant, domácí), Katarína KEJSTOVÁ (703 Slovensko, domácí), Tadeáš KUČERA (203 Česká republika, domácí), Henrich LAUKO (703 Slovensko, domácí), Jan MRÁZEK (203 Česká republika, domácí), Petr ROČKAI (703 Slovensko, domácí) a Vladimír ŠTILL (203 Česká republika, domácí).
Vydání Cham, Automated Technology for Verification and Analysis, od s. 201-207, 7 s. 2017.
Nakladatel Springer International Publishing
Další údaje
Originální 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"
WWW URL
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/17:00095126
Organizační jednotka Fakulta informatiky
ISBN 978-3-319-68166-5
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-68167-2_14
Klíčová slova anglicky Model Checking; Verification; C; C++; DIVINE
Štítky firank_A
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 1. 10. 2018 16:24.
Anotace
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 VaVNázev: Analýza korektnosti vícevláknových programů v C a C++
Investor: Grantová agentura ČR, Standardní projekty
MUNI/A/0897/2016, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.
Investor: Masarykova univerzita, Grantová agentura MU, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0992/2016, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Grantová agentura MU, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 6. 12. 2021 18:50