Publication details
Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
Authors | |
---|---|
Year of publication | 2017 |
Type | Article in Proceedings |
Conference | Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017, Part II |
MU Faculty or unit | |
Citation | |
Web | https://link.springer.com/chapter/10.1007/978-3-662-54580-5_29 |
Doi | http://dx.doi.org/10.1007/978-3-662-54580-5_29 |
Field | Informatics |
Keywords | program verification; model checking; formula optimizations; caching |
Description | 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. |
Related projects: |