@inbook{MJSLB2017,
 _booksubtitle = {23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II},
 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.},
 address = {Berlin, Heidelberg},
 author = {Jan Mrázek and Martin Jonáš and Vladimír Štill and Henrich Lauko and Jiří Barnat},
 booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
 doi = {10.1007/978-3-662-54580-5_29},
 editor = {Legay, Axel
and Margaria, Tiziana},
 isbn = {978-3-662-54580-5},
 keywords = {divine,symdivine},
 pages = {390--393},
 publisher = {Springer Berlin Heidelberg},
 title = {{Optimizing and Caching SMT Queries in SymDIVINE}},
 url = {https://doi.org/10.1007/978-3-662-54580-5_29},
 year = {2017}
}