Abstract
The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.
This work has been partially supported by the Czech Science Foundation grant No. 15-08772S and by Red Hat, Inc.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Available from https://github.com/xlauko/dipot.
- 2.
- 3.
- 4.
The binary has to be in a directory which is listed in the PATH environment variable.
- 5.
References
Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0—a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016). doi:10.1007/978-3-319-46520-3_8
Mrázek, J., Bauch, P., Lauko, H., Barnat, J.: SymDIVINE: tool for control-explicit data-symbolic state space exploration. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 208–213. Springer, Cham (2016). doi:10.1007/978-3-319-32582-8_14
Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L., Fischer, B.: SMT-based bounded model checking of C++ programs. In: Engineering of Computer Based Systems (ECBS), pp. 147–156. IEEE Computer Society (2013)
Ročkai, P., Barnat, J.: A Simulator for LLVM Bitcode. Preliminary version, arXiv:1704.05551 (2017)
Ročkai, P., Barnat, J., Brim, L.: Improved state space reductions for LTL model checking of C & C++ programs. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013, vol. 7871, pp. 1–15. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38088-4_1
Ročkai, P., Štill, V., Černá, I., Barnat, J.: DiVM: Model Checking with LLVM and Graph Memory. Preliminary version, arXiv:1703.05341 (2017)
Štill, V., Ročkai, P., Barnat, J.: Weak memory models as LLVM-to-LLVM transformations. In: Kofroň, J., Vojnar, T. (eds.) MEMICS 2015. LNCS, vol. 9548, pp. 144–155. Springer, Cham (2016). doi:10.1007/978-3-319-29817-7_13
Štill, V., Ročkai, P., Barnat, J.: Using off-the-shelf exception support components in C++ verification. In: IEEE International Conference on Software Quality, Reliability and Security (QRS 2017) (2017). doi:10.1109/QRS.2017.15
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Baranová, Z. et al. (2017). Model Checking of C and C++ with DIVINE 4. In: D'Souza, D., Narayan Kumar, K. (eds) Automated Technology for Verification and Analysis. ATVA 2017. Lecture Notes in Computer Science(), vol 10482. Springer, Cham. https://doi.org/10.1007/978-3-319-68167-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-68167-2_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68166-5
Online ISBN: 978-3-319-68167-2
eBook Packages: Computer ScienceComputer Science (R0)