MRÁZEK, Jan, Martin JONÁŠ, Vladimír ŠTILL, Henrich LAUKO and 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. p. 390-393. ISBN 978-3-662-54579-9. doi:10.1007/978-3-662-54580-5_29.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
Authors MRÁZEK, Jan (203 Czech Republic, belonging to the institution), Martin JONÁŠ (203 Czech Republic, belonging to the institution), Vladimír ŠTILL (203 Czech Republic, belonging to the institution), Henrich LAUKO (703 Slovakia, belonging to the institution) and Jiří BARNAT (203 Czech Republic, guarantor, belonging to the institution).
Edition Berlin, Heidelberg, Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017, Part II, p. 390-393, 4 pp. 2017.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
WWW URL
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/17:00095131
Organization unit Faculty of Informatics
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
Keywords in English program verification; model checking; formula optimizations; caching
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 13/5/2020 19:23.
Abstract
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.
Links
GA15-08772S, research and development projectName: Analýza korektnosti vícevláknových programů v C a C++
Investor: Czech Science Foundation, Standard Projects
MUNI/A/0897/2016, internal MU codeName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
MUNI/A/0992/2016, internal MU codeName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
PrintDisplayed: 16/1/2022 11:24