Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1394228,
author = {Mrázek, Jan and Jonáš, Martin and Štill, Vladimír and Lauko, Henrich and Barnat, Jiří},
address = {Berlin, Heidelberg},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017, Part II},
doi = {http://dx.doi.org/10.1007/978-3-662-54580-5_29},
editor = {Axel Legay, Tiziana Margaria},
keywords = {program verification; model checking; formula optimizations; caching},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Berlin, Heidelberg},
isbn = {978-3-662-54579-9},
pages = {390-393},
publisher = {Springer},
title = {Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)},
url = {https://link.springer.com/chapter/10.1007/978-3-662-54580-5_29},
year = {2017}
}
TY - JOUR
ID - 1394228
AU - Mrázek, Jan - Jonáš, Martin - Štill, Vladimír - Lauko, Henrich - Barnat, Jiří
PY - 2017
TI - Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
PB - Springer
CY - Berlin, Heidelberg
SN - 9783662545799
KW - program verification
KW - model checking
KW - formula optimizations
KW - caching
UR - https://link.springer.com/chapter/10.1007/978-3-662-54580-5_29
N2 - 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.
ER -
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. \textit{Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017, Part II}. Berlin, Heidelberg: Springer. p.~390-393. ISBN~978-3-662-54579-9. doi:10.1007/978-3-662-54580-5\_{}29. 2017.
|
