Abstract
We describe the new features of the bounded model checker Dartagnan for SV-COMP ’21. We participate, for the first time, in the ReachSafety category on the verification of sequential programs. In some of these verification tasks, bugs only show up after many loop iterations, which is a challenge for bounded model checking. We address the challenge by simplifying the structure of the input program while preserving its semantics. For simplification, we leverage common compiler optimizations, which we get for free by using LLVM. Yet, there is a price to pay. Compiler optimizations may introduce bitwise operations, which require bit-precise reasoning. We evaluated an SMT encoding based on the theory of integers + bit conversions against one based on the theory of bit-vectors and found that the latter yields better performance. Compared to the unoptimized version of Dartagnan, the combination of compiler optimizations and bit-vectors yields a speed-up of an order of magnitude on average.
H. Ponce-de-León—Jury member.
Chapter PDF
Similar content being viewed by others
References
D. Beyer. Software verification: 10th comparative evaluation (SV-COMP 2021). In Proc. TACAS (2), LNCS 12652. Springer, 2021.
Dirk Beyer, Stefan Löwe, and Philipp Wendler. Reliable benchmarking: requirements and solutions. STTT, 21(1), 1–29, 2019. https://doi.org/10.1007/s10009-017-0469-y.
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, and Roland Meyer. Dartagnan: Bounded model checking for weak memory models (competition contribution). In TACAS (2), volume 12079 of LNCS, pages 378–382. Springer, 2020. https://doi.org/10.1007/978-3-030-45237-7_24.
Natalia Gavrilenko, Hernán Ponce de León, Florian Furbach, Keijo Heljanko, and Roland Meyer. BMC for weak memory models: Relation analysis for compact SMT encodings. In CAV, volume 11561 of LNCS, pages 355–365. Springer, 2019. https://doi.org/10.1007/978-3-030-25540-4_19.
Shaobo He and Zvonimir Rakamaric. Counterexample-guided bit-precision selection. In APLAS, volume 10695 of LNCS, pages 534–553. Springer, 2017. https://doi.org/10.1007/978-3-319-71237-6_26.
Timotej Kapus, Martin Nowack, and Cristian Cadar. Constraints in dynamic symbolic execution: Bitvectors or integers? In TAP@FM, volume 11823 of LNCS, pages 41–54. Springer, 2019. https://doi.org/10.1007/978-3-030-31157-5_3.
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, and Roland Meyer. Portability analysis for weak memory models. PORTHOS: One tool for all models. In SAS, volume 10422 of LNCS, pages 299–320. Springer, 2017. https://doi.org/10.1007/978-3-319-66706-5_15.
Zvonimir Rakamaric and Michael Emmi. SMACK: Decoupling source language details from verifier implementations. In CAV, volume 8559 of LNCS, pages 106–113. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_7.
Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli. Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In POPL, pages 209–220. ACM, 2015. https://doi.org/10.1145/2676726.2676995.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Ponce-de-León, H., Haas, T., Meyer, R. (2021). Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution). In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12652. Springer, Cham. https://doi.org/10.1007/978-3-030-72013-1_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-72013-1_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72012-4
Online ISBN: 978-3-030-72013-1
eBook Packages: Computer ScienceComputer Science (R0)