{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:09Z","timestamp":1779087669877,"version":"3.51.4"},"publisher-location":"Cham","reference-count":9,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720124","type":"print"},{"value":"9783030720131","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe the new features of the bounded model checker<jats:sc>Dartagnan<\/jats:sc>for<jats:sc>SV-COMP<\/jats:sc>\u201921. We participate, for the first time, in the<jats:italic>ReachSafety<\/jats:italic>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<jats:sc>Dartagnan<\/jats:sc>, the combination of compiler optimizations and bit-vectors yields a speed-up of an order of magnitude on average.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_26","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"428-432","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (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":[[2021,3,23]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"D. Beyer. Software verification: 10th comparative evaluation (SV-COMP 2021). In Proc. TACAS (2), LNCS 12652. Springer, 2021.","DOI":"10.1007\/978-3-030-72013-1_24"},{"key":"26_CR2","doi-asserted-by":"publisher","unstructured":"Dirk Beyer, Stefan L\u00f6we, and Philipp Wendler. Reliable benchmarking: requirements and solutions. STTT, 21(1), 1\u201329, 2019. https:\/\/doi.org\/10.1007\/s10009-017-0469-y.","DOI":"10.1007\/s10009-017-0469-y"},{"key":"26_CR3","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"},{"key":"26_CR4","doi-asserted-by":"publisher","unstructured":"Natalia Gavrilenko, Hern\u00e1n Ponce de Le\u00f3n, 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\u2013365. Springer, 2019. https:\/\/doi.org\/10.1007\/978-3-030-25540-4_19.","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"26_CR5","doi-asserted-by":"publisher","unstructured":"Shaobo He and Zvonimir Rakamaric. Counterexample-guided bit-precision selection. In APLAS, volume 10695 of LNCS, pages 534\u2013553. Springer, 2017. https:\/\/doi.org\/10.1007\/978-3-319-71237-6_26.","DOI":"10.1007\/978-3-319-71237-6_26"},{"key":"26_CR6","doi-asserted-by":"publisher","unstructured":"Timotej Kapus, Martin Nowack, and Cristian Cadar. Constraints in dynamic symbolic execution: Bitvectors or integers? In TAP@FM, volume 11823 of LNCS, pages 41\u201354. Springer, 2019. https:\/\/doi.org\/10.1007\/978-3-030-31157-5_3.","DOI":"10.1007\/978-3-030-31157-5_3"},{"key":"26_CR7","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":"26_CR8","doi-asserted-by":"publisher","unstructured":"Zvonimir Rakamaric and Michael Emmi. SMACK: Decoupling source language details from verifier implementations. In CAV, volume 8559 of LNCS, pages 106\u2013113. Springer, 2014. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7.","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"26_CR9","doi-asserted-by":"publisher","unstructured":"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\u2013220. ACM, 2015. https:\/\/doi.org\/10.1145\/2676726.2676995.","DOI":"10.1145\/2676726.2676995"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72013-1_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T00:08:22Z","timestamp":1619741302000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/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":"141","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":"41","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":"21","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":"12","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":"The conference changed to an online format due to the COVID-19 pandemic","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)"}}]}}