{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,12]],"date-time":"2026-08-12T04:40:12Z","timestamp":1786509612182,"version":"3.56.0"},"publisher-location":"Cham","reference-count":10,"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><jats:sc>Ultimate GemCutter<\/jats:sc> verifies concurrent programs using the CEGAR paradigm, by generalizing from spurious counterexample traces to larger sets of correct traces. We integrate classical CEGAR generalization with orthogonal generalization across interleavings. Thereby, we are able to prove correctness of programs otherwise out-of-reach for interpolation-based verification. The competition results show significant advantages over other concurrency approaches in the <jats:sc>Ultimate<\/jats:sc> family.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_35","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"479-483","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Ultimate GemCutter and the Axes of Generalization"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4885-0728","authenticated-orcid":false,"given":"Dominik","family":"Klumpp","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8947-5373","authenticated-orcid":false,"given":"Daniel","family":"Dietsch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4252-3558","authenticated-orcid":false,"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5656-306X","authenticated-orcid":false,"given":"Frank","family":"Sch\u00fcssele","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marcel","family":"Ebbinghaus","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Azadeh","family":"Farzan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2540-9489","authenticated-orcid":false,"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"35_CR1","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS\u00a0(2). Springer (2022)","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"35_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","DOI":"10.1007\/s10009-017-0469-y"},{"key":"35_CR3","doi-asserted-by":"publisher","unstructured":"Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific (1995). https:\/\/doi.org\/10.1142\/2563","DOI":"10.1142\/2563"},{"key":"35_CR4","doi-asserted-by":"publisher","unstructured":"Farzan, A., Vandikas, A.: Automated hypersafety verification. In: CAV (1). Lecture Notes in Computer Science, vol. 11561, pp. 200\u2013218. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_11","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"35_CR5","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, Lecture Notes in Computer Science, vol.\u00a01032. Springer (1996). https:\/\/doi.org\/10.1007\/3-540-60761-7","DOI":"10.1007\/3-540-60761-7"},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"He, F., Sun, Z., Fan, H.: Deagle: An SMT-based verifier for multi-threaded programs (competition contribution). In: Proc. TACAS\u00a0(2). Springer (2022)","DOI":"10.1007\/978-3-030-99527-0_25"},{"key":"35_CR7","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Chen, Y., Dietsch, D., Greitschus, M., Nutz, A., Musa, B., Sch\u00e4tzle, C., Schilling, C., Sch\u00fcssele, F., Podelski, A.: Ultimate Automizer with an on-demand construction of Floyd-Hoare automata - (competition contribution). In: TACAS (2). Lecture Notes in Computer Science, vol. 10206, pp. 394\u2013398 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_30","DOI":"10.1007\/978-3-662-54580-5_30"},{"key":"35_CR8","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: SAS. Lecture Notes in Computer Science, vol.\u00a05673, pp. 69\u201385. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03237-0_7","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"35_CR9","doi-asserted-by":"publisher","unstructured":"Klumpp, D., Dietsch, D., Heizmann, M., Sch\u00fcssele, F., Ebbinghaus, M., Farzan, A., Podelski, A.: Ultimate GemCutter SV-COMP 2022 Competition Contribution (Nov 2021). https:\/\/doi.org\/10.5281\/zenodo.5956945","DOI":"10.5281\/zenodo.5956945"},{"key":"35_CR10","unstructured":"Sales, E., Coto, A., Inverso, O., Tuosto, E.: A prototype for data race detection in CSeq 3 (competition contribution). In: Proc. TACAS\u00a0(2). Springer (2022)"}],"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_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:50:58Z","timestamp":1710233458000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_35"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_35","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)"}}]}}