Abstract
Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.
H. Ponce-de-León—Jury member.
Chapter PDF
Similar content being viewed by others
References
The herdtools7 tool suite. https://github.com/herd/herdtools7.
Jade Alglave, Patrick Cousot, and Luc Maranget. Syntax and semantics of the weak consistency model specification language CAT. CoRR, abs/1608.07531, 2016.
Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008.
Natalia Gavrilenko. Improving scalability of bounded model checking for weak memory models. Master’s thesis, Aalto University, Department of Computer Science, 2019.
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.
Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean Pichon-Pharabod, and Peter Sewell. Cerberus-BMC: A principled reference semantics and exploration tool for concurrent and sequential C. In CAV, volume 11561 of LNCS, pages 387–397. Springer, 2019.
K. Rustan M. Leino. This is Boogie 2. 2008.
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.
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, and Roland Meyer. BMC with memory models as modules. In FMCAD, pages 1–9. IEEE, 2018.
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, and Roland Meyer. Replication package for the Dartagnan tool for SVCOMP 2020. http://dx.doi.org/10.5281/zenodo.3678318, February 2020.
Zvonimir Rakamaric and Michael Emmi. SMACK: Decoupling source language details from verifier implementations. In CAV, volume 8559 of LNCS, pages 106–113. Springer, 2014.
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
© 2020 The Author(s)
About this paper
Cite this paper
Ponce-de-León, H., Furbach, F., Heljanko, K., Meyer, R. (2020). Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution). In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12079. Springer, Cham. https://doi.org/10.1007/978-3-030-45237-7_24
Download citation
DOI: https://doi.org/10.1007/978-3-030-45237-7_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45236-0
Online ISBN: 978-3-030-45237-7
eBook Packages: Computer ScienceComputer Science (R0)