Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1352238, author = {Mrázek, Jan and Bauch, Petr and Lauko, Henrich and Barnat, Jiří}, address = {Neuveden}, booktitle = {Model Checking Software}, doi = {http://dx.doi.org/10.1007/978-3-319-32582-8_14}, editor = {Dragan Bošnački and Anton Wijs}, keywords = {Model checking; C++; Symbolic approach}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Neuveden}, isbn = {978-3-319-32581-1}, pages = {208-213}, publisher = {Springer International Publishing}, title = {SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration}, year = {2016} }
TY - JOUR ID - 1352238 AU - Mrázek, Jan - Bauch, Petr - Lauko, Henrich - Barnat, Jiří PY - 2016 TI - SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration PB - Springer International Publishing CY - Neuveden SN - 9783319325811 KW - Model checking KW - C++ KW - Symbolic approach N2 - We present SymDIVINE: a tool for bit-precise model checking of parallel C and C++ programs. It builds upon LLVM compiler infrastructure, hence, it uses LLVM IR as an input formalism. Internally, SymDIVINE extends the standard explicit-state state space exploration with SMT machinery to handle non-deterministic data values. As such, SymDIVINE is on a halfway between a symbolic executor and an explicit-state model checker. The key differentiating aspect present in SymDIVINE is the ability to decide about equality of two symbolically represented states preventing thus repeated exploration of the state space graph. This is crucially important in particular for verification of parallel programs where the state space graph is full of diamond-shaped subgraphs. ER -
MRÁZEK, Jan, Petr BAUCH, Henrich LAUKO and Jiří BARNAT. SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. In Dragan Bošnački and Anton Wijs. \textit{Model Checking Software}. Neuveden: Springer International Publishing, 2016, p.~208-213. ISBN~978-3-319-32581-1. Available from: https://dx.doi.org/10.1007/978-3-319-32582-8\_{}14.
|