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: |