Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
| Autoři | |
|---|---|
| Rok publikování | 2017 |
| Druh | Článek ve sborníku |
| Konference | Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017, Part II |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | 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 |
| Obor | Informatika |
| Klíčová slova | program verification; model checking; formula optimizations; caching |
| Popis | 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. |
| Související projekty: |