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, 2017, p.~390-393. ISBN~978-3-662-54579-9. Available from: https://dx.doi.org/10.1007/978-3-662-54580-5\_{}29.
|