MRÁZEK, Jan, Martin JONÁŠ, Vladimír ŠTILL, Henrich LAUKO a Jiří BARNAT. Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution). In Axel Legay, Tiziana Margaria. Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017, Part II. Berlin, Heidelberg: Springer, 2017. s. 390-393. ISBN 978-3-662-54579-9. doi:10.1007/978-3-662-54580-5_29.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
Autoři MRÁZEK, Jan (203 Česká republika, domácí), Martin JONÁŠ (203 Česká republika, domácí), Vladimír ŠTILL (203 Česká republika, domácí), Henrich LAUKO (703 Slovensko, domácí) a Jiří BARNAT (203 Česká republika, garant, domácí).
Vydání Berlin, Heidelberg, Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017, Part II, od s. 390-393, 4 s. 2017.
Nakladatel Springer
Další údaje
Originální 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"
WWW URL
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/17:00095131
Organizační jednotka Fakulta informatiky
ISBN 978-3-662-54579-9
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-662-54580-5_29
UT WoS 000440733400029
Klíčová slova anglicky program verification; model checking; formula optimizations; caching
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 13. 5. 2020 19:23.
Anotace
This paper presents a new version of the tool SymDIVINE, a model-checker for concurrent C/C++ programs. SymDIVINE uses a control-explicit data-symbolic approach to model checking, which allows for the bit-precise verification of programs with inputs, by representing data part of a program state by a first-order bit-vector formula. The new version of the tool employs a refined representation of symbolic states, which allows for efficient caching of smt queries. Moreover, the new version employs additional simplifications of first-order bit-vector formulas, such as elimination of unconstrained variables from quantified formulas. All changes are documented in detail in the paper.
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: 9. 12. 2021 14:54