Abstract
The validation of violation witnesses is an important step during software verification. It hides false alarms raised by verifiers from engineers, which in turn helps them concentrate on critical issues and improves the verification experience. Until the 2021 edition of the Competition on Software Verification (SV-COMP), CPAchecker was the only witness validator for the ConcurrencySafety category. This article describes how we extended the Dartagnan verifier to support the validation of violation witnesses. The results of the 2022 edition of the competition show that, for witnesses generated by different verifiers, Dartagnan succeeds in the validation of witnesses where CPAchecker does not. Our extension thus improves the validation possibilities for the overall competition. We discuss Dartagnan ’s strengths and weaknesses as a validation tool and describe possible ways to improve it in the future.
Hernán Ponce-de-León : Jury member.
Chapter PDF
Similar content being viewed by others
References
Exchange Format for Violation Witnesses and Correctness Witnesses. https://github.com/sosy-lab/sv-witnesses.
Fatimah Aljaafari, Lucas C. Cordeiro, Mustafa A. Mustafa, and Rafael Menezes. EBF: A hybrid verification tool for finding software vulnerabilities in iot cryptographic protocols. CoRR, abs/2103.11363, 2021.
Pavel S. Andrianov, Vadim S. Mutilin, and Alexey V. Khoroshilov. cpalockator: Thread-modular analysis with projections - (Competition Contribution). In TACAS (2), volume 12652 of Lecture Notes in Computer Science, pages 423–427. Springer, 2021. https://doi.org/10.1007/978-3-030-72013-1_25.
Dirk Beyer. Software verification and verifiable witnesses - (report on SV-COMP 2015). In TACAS, volume 9035 of Lecture Notes in Computer Science, pages 401–416. Springer, 2015. https://doi.org/10.1007/978-3-662-46681-0_31.
Dirk Beyer. Progress on software verification: SV-COMP 2022. In TACAS (2). Springer, 2022.
Dirk Beyer. Verifiers and validators of the 11th Intl. Competition on Software Verification (SV-COMP 2022). Zenodo, 2022. https://doi.org/10.5281/zenodo.5959149.
Dirk Beyer and M. Erkan Keremoglu. CPAchecker: A tool for configurable software verification. In CAV, volume 6806 of Lecture Notes in Computer Science, pages 184–190. Springer, 2011. https://doi.org/10.1007/978-3-642-22110-1_16.
Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schätzle, and Frank Schüssele. Ultimate Taipan with symbolic interpretation and fluid abstractions - (C ompetition Contribution). In TACAS (2), volume 12079 of Lecture Notes in Computer Science, pages 418–422. Springer, 2020. https://doi.org/10.1007/978-3-030-45237-7_32.
Fei He, Zhihang Sun, and Hongyu Fan. Deagle: An SMT-based verifier for multi-threaded programs (Competition Contribution). In TACAS (2). Springer, 2022.
Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, and Andreas Podelski. Ultimate Automizer and the search for perfect interpolants - (Competition Contribution). In TACAS (2), volume 10806 of Lecture Notes in Computer Science, pages 447–451. Springer, 2018. https://doi.org/10.1007/978-3-319-89963-3_30.
Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. Lazy-CSeq: A lazy sequentialization tool for C - (Competition Contribution). In TACAS, volume 8413 of Lecture Notes in Computer Science, pages 398–401. Springer, 2014. https://doi.org/10.1007/978-3-642-36742-7_46.
Dominik Klumpp, Daniel Dietsch, Matthias Heizmann, Frank Schüssele, Marcel Ebbinghaus, Azadeh Farzan, and Andreas Podelski. Ultimate GemCutter and the axes of generalization (Competition Contribution). In TACAS (2). Springer, 2022.
Daniel Kroening and Michael Tautschnig. CBMC - C bounded model checker - (Competition Contribution). In TACAS, volume 8413 of Lecture Notes in Computer Science, pages 389–391. Springer, 2014. https://doi.org/10.1007/978-3-642-54862-8_26.
William Leeson and Matthew Dwyer. GraVeS: Graph-based verifier selector (Competition Contribution). In TACAS (2). Springer, 2022.
K. Rustan M. Leino. This is Boogie 2. 2008. URL: https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/.
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.
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.
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
© 2022 The Author(s)
About this paper
Cite this paper
Ponce-de-León, H., Haas, T., Meyer, R. (2022). Dartagnan: SMT-based Violation Witness Validation (Competition Contribution). In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13244. Springer, Cham. https://doi.org/10.1007/978-3-030-99527-0_24
Download citation
DOI: https://doi.org/10.1007/978-3-030-99527-0_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99526-3
Online ISBN: 978-3-030-99527-0
eBook Packages: Computer ScienceComputer Science (R0)