{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:31Z","timestamp":1776305371696,"version":"3.50.1"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995263","type":"print"},{"value":"9783030995270","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 (<jats:sc>SV-COMP<\/jats:sc>), <jats:sc>CPAchecker<\/jats:sc> was the only witness validator for the <jats:italic>ConcurrencySafety<\/jats:italic> category. This article describes how we extended the <jats:sc>Dartagnan<\/jats:sc> 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, <jats:sc>Dartagnan<\/jats:sc> succeeds in the validation of witnesses where <jats:sc>CPAchecker<\/jats:sc> does not. Our extension thus improves the validation possibilities for the overall competition. We discuss <jats:sc>Dartagnan<\/jats:sc> \u2019s strengths and weaknesses as a validation tool and describe possible ways to improve it in the future.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_24","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"418-423","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Dartagnan: SMT-based Violation Witness Validation (Competition Contribution)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8830","authenticated-orcid":false,"given":"Hern\u00e1n","family":"Ponce-de-Le\u00f3n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3176-8552","authenticated-orcid":false,"given":"Thomas","family":"Haas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8495-671X","authenticated-orcid":false,"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"24_CR1","unstructured":"Exchange Format for Violation Witnesses and Correctness Witnesses. https:\/\/github.com\/sosy-lab\/sv-witnesses."},{"key":"24_CR2","unstructured":"Fatimah Aljaafari, Lucas\u00a0C. Cordeiro, Mustafa\u00a0A. Mustafa, and Rafael Menezes. EBF: A hybrid verification tool for finding software vulnerabilities in iot cryptographic protocols. CoRR, abs\/2103.11363, 2021."},{"key":"24_CR3","doi-asserted-by":"publisher","unstructured":"Pavel\u00a0S. Andrianov, Vadim\u00a0S. Mutilin, and Alexey\u00a0V. Khoroshilov. cpalockator: Thread-modular analysis with projections - (Competition Contribution). In TACAS (2), volume 12652 of Lecture Notes in Computer Science, pages 423\u2013427. Springer, 2021. https:\/\/doi.org\/10.1007\/978-3-030-72013-1_25.","DOI":"10.1007\/978-3-030-72013-1_25"},{"key":"24_CR4","doi-asserted-by":"publisher","unstructured":"Dirk Beyer. Software verification and verifiable witnesses - (report on SV-COMP 2015). In TACAS, volume 9035 of Lecture Notes in Computer Science, pages 401\u2013416. Springer, 2015. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_31.","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Dirk Beyer. Progress on software verification: SV-COMP 2022. In TACAS (2). Springer, 2022.","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"24_CR6","doi-asserted-by":"publisher","unstructured":"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.","DOI":"10.5281\/zenodo.5959149"},{"key":"24_CR7","doi-asserted-by":"publisher","unstructured":"Dirk Beyer and M.\u00a0Erkan Keremoglu. CPAchecker: A tool for configurable software verification. In CAV, volume 6806 of Lecture Notes in Computer Science, pages 184\u2013190. Springer, 2011. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16.","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"24_CR8","doi-asserted-by":"publisher","unstructured":"Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Sch\u00e4tzle, and Frank Sch\u00fcssele. Ultimate Taipan with symbolic interpretation and fluid abstractions - (C ompetition Contribution). In TACAS (2), volume 12079 of Lecture Notes in Computer Science, pages 418\u2013422. Springer, 2020. https:\/\/doi.org\/10.1007\/978-3-030-45237-7_32.","DOI":"10.1007\/978-3-030-45237-7_32"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Fei He, Zhihang Sun, and Hongyu Fan. Deagle: An SMT-based verifier for multi-threaded programs (Competition Contribution). In TACAS (2). Springer, 2022.","DOI":"10.1007\/978-3-030-99527-0_25"},{"key":"24_CR10","doi-asserted-by":"publisher","unstructured":"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\u2013451. Springer, 2018. https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30.","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"24_CR11","doi-asserted-by":"publisher","unstructured":"Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore\u00a0La 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\u2013401. Springer, 2014. https:\/\/doi.org\/10.1007\/978-3-642-36742-7_46.","DOI":"10.1007\/978-3-642-36742-7_46"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Dominik Klumpp, Daniel Dietsch, Matthias Heizmann, Frank Sch\u00fcssele, Marcel Ebbinghaus, Azadeh Farzan, and Andreas Podelski. Ultimate GemCutter and the axes of generalization (Competition Contribution). In TACAS (2). Springer, 2022.","DOI":"10.1007\/978-3-030-99527-0_35"},{"key":"24_CR13","doi-asserted-by":"publisher","unstructured":"Daniel Kroening and Michael Tautschnig. CBMC - C bounded model checker - (Competition Contribution). In TACAS, volume 8413 of Lecture Notes in Computer Science, pages 389\u2013391. Springer, 2014. https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26.","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"William Leeson and Matthew Dwyer. GraVeS: Graph-based verifier selector (Competition Contribution). In TACAS (2). Springer, 2022.","DOI":"10.1007\/978-3-030-99527-0_28"},{"key":"24_CR15","unstructured":"K.\u00a0Rustan\u00a0M. Leino. This is Boogie 2. 2008. URL: https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/."},{"key":"24_CR16","doi-asserted-by":"publisher","unstructured":"Hern\u00e1n Ponce de Le\u00f3n, 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\u2013320. Springer, 2017. https:\/\/doi.org\/10.1007\/978-3-319-66706-5_15.","DOI":"10.1007\/978-3-319-66706-5_15"},{"key":"24_CR17","doi-asserted-by":"publisher","unstructured":"Hern\u00e1n Ponce de Le\u00f3n, 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\u2013382. Springer, 2020. https:\/\/doi.org\/10.1007\/978-3-030-45237-7_24.","DOI":"10.1007\/978-3-030-45237-7_24"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99527-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:49:54Z","timestamp":1710233394000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}