{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:04Z","timestamp":1776305344322,"version":"3.50.1"},"publisher-location":"Cham","reference-count":83,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031826993","type":"print"},{"value":"9783031827006","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-82700-6_4","type":"book-chapter","created":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T01:26:23Z","timestamp":1737595583000},"page":"74-100","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts"],"prefix":"10.1007","author":[{"given":"Julian","family":"Erhard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Bentele","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominik","family":"Klumpp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simmo","family":"Saan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Sch\u00fcssele","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Schwarz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarah","family":"Tilscher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vesal","family":"Vojdani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,1,24]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-540-32275-7_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"E Albert","year":"2005","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.: Abstraction-carrying code. In: Baader, F., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3452, pp. 380\u2013397. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_25"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Apt, K.R., de\u00a0Boer, F.S., Olderog, E.: Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer (2009). ISBN 978-1-84882-744-8. https:\/\/doi.org\/10.1007\/978-1-84882-745-5","DOI":"10.1007\/978-1-84882-745-5"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Ayaziov\u00e1, P., Beyer, D., Lingsch-Rosenfeld, M., Spiessl, M., Strej\u010dek, J.: Software verification witnesses 2.0. In: Model Checking Software. Lecture Notes in Computer Science, vol. 14624, pp. 184\u2013203. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-66149-5_11","DOI":"10.1007\/978-3-031-66149-5_11"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-030-41600-3_8","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"B Becker","year":"2020","unstructured":"Becker, B., March\u00e9, C.: Ghost code in action: automated verification of a symbolic interpreter. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 107\u2013123. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_8"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP\u00a02023. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 495\u2013522, Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Luxembourg City, Luxembourg, 6\u201311 April 2024, Proceedings, Part III. Lecture Notes in Computer Science, vol. 14572, pp. 299\u2013329. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"4_CR7","unstructured":"Beyer, D.: SV-COMP 2024 - 13th competition on software verification (2024). https:\/\/sv-comp.sosy-lab.org\/2024\/rules.php. Accessed 29 Sept 2024"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, 13\u201318 November 2016, pp. 326\u2013337. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Nitto, E.D., Harman, M., Heymans, P. (eds.) Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2015, Bergamo, Italy, 30 August\u20134 September 2015, pp. 721\u2013733. ACM (2015). https:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-030-61362-4_26","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"D Beyer","year":"2020","unstructured":"Beyer, D., Friedberger, K.: Violation witnesses and result validation for multi-threaded programs. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 449\u2013470. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_26"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/978-3-030-99524-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2022","unstructured":"Beyer, D., Kanav, S.: CoVeriTeam: on-demand composition of cooperative verification systems. In: TACAS 2022. LNCS, vol. 13243, pp. 561\u2013579. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_31"},{"issue":"1","key":"4_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2017","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1\u201329 (2017). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-030-99336-8_9","volume-title":"Programming Languages and Systems","author":"EV Bila","year":"2022","unstructured":"Bila, E.V., Dongol, B., Lahav, O., Raad, A., Wickerson, J.: View-based Owicki\u2013Gries reasoning for persistent x86-TSO. In: ESOP 2022. LNCS, vol. 13240, pp. 234\u2013261. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_9"},{"issue":"1\u20133","key":"4_CR14","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/J.TCS.2006.12.034","volume":"375","author":"S Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1\u20133), 227\u2013270 (2007). https:\/\/doi.org\/10.1016\/J.TCS.2006.12.034","journal-title":"Theor. Comput. Sci."},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Brookes, S.: On grainless footprint semantics for shared-memory programs. In: Jacobs, B., Silva, A., Staton, S. (eds.) Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2014, Ithaca, NY, USA, 12\u201315 June 2014. Electronic Notes in Theoretical Computer Science, vol. 308, pp. 65\u201386. Elsevier (2014). https:\/\/doi.org\/10.1016\/J.ENTCS.2014.10.005","DOI":"10.1016\/J.ENTCS.2014.10.005"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-642-14052-5_3","volume-title":"Interactive Theorem Proving","author":"D Cachera","year":"2010","unstructured":"Cachera, D., Pichardie, D.: A certified denotational abstract interpreter. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 9\u201324. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_3"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-030-68446-4_14","volume-title":"Logic-Based Program Synthesis and Transformation","author":"I Casso","year":"2021","unstructured":"Casso, I., Morales, J.F., L\u00f3pez-Garc\u00eda, P., Hermenegildo, M.V.: Testing your (static analysis) truths. In: LOPSTR 2020. LNCS, vol. 12561, pp. 271\u2013292. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-68446-4_14"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Clarke, E.M.: Synthesis of resource invariants for concurrent programs. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979, pp. 211\u2013221. ACM Press (1979). https:\/\/doi.org\/10.1145\/567752.567772","DOI":"10.1145\/567752.567772"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Correnson, A., Steinh\u00f6fel, D.: Engineering a formally verified automated bug finder. In: Chandra, S., Blincoe, K., Tonella, P. (eds.) Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2023, San Francisco, CA, USA, 3\u20139 December 2023, pp. 1165\u20131176. ACM (2023). https:\/\/doi.org\/10.1145\/3611643.3616290","DOI":"10.1145\/3611643.3616290"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Dalvandi, S., Doherty, S., Dongol, B., Wehrheim, H.: Owicki-Gries reasoning for C11 RAR. In: Hirschfeld, R., Pape, T. (eds.) 34th European Conference on Object-Oriented Programming, ECOOP 2020, 15\u201317 November 2020, Berlin, Germany (Virtual Conference). LIPIcs, vol. 166, pp. 11:1\u201311:26, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2020.11","DOI":"10.4230\/LIPICS.ECOOP.2020.11"},{"issue":"1","key":"4_CR21","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/S10817-021-09610-2","volume":"66","author":"S Dalvandi","year":"2022","unstructured":"Dalvandi, S., Dongol, B., Doherty, S., Wehrheim, H.: Integrating Owicki-Gries for C11-style memory models into Isabelle\/HOL. J. Autom. Reason. 66(1), 141\u2013171 (2022). https:\/\/doi.org\/10.1007\/S10817-021-09610-2","journal-title":"J. Autom. Reason."},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Dijkstra, E.W.: Finding the correctness proof of a concurrent program. In: Bauer, F.L., Broy, M. (eds.) Program Construction, International Summer School, July 26 - August 6, 1978, Marktoberdorf, Germany, Lecture Notes in Computer Science, vol.\u00a069, pp. 24\u201334, Springer (1978). https:\/\/doi.org\/10.1007\/BFB0014652","DOI":"10.1007\/BFB0014652"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Erhard, J., et al.: Artifact for the VMCAI\u20192025 paper \u201cCorrectness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts\u201d (2024). https:\/\/doi.org\/10.5281\/zenodo.13863579","DOI":"10.5281\/zenodo.13863579"},{"key":"4_CR24","unstructured":"Erhard, J., et al.: Correctness witness schema (2024). https:\/\/ultimate-pa.github.io\/concurrency-witnesses\/correctness-witness-schema.yml. Accessed 29 Sept 2024"},{"key":"4_CR25","unstructured":"Erhard, J., et al.: Correctness witnesses for concurrent programs: bridging the semantic divide with ghosts (extended version) (2024). https:\/\/doi.org\/10.48550\/arXiv.2411.16612"},{"key":"4_CR26","unstructured":"Erhard, J., et al.: Format for correctness witnesses, version 2.1 (2024). ultimate-pa.github.io\/concurrency-witnesses\/index.html. Accessed 29 Sept 2024"},{"key":"4_CR27","unstructured":"Evans, C., Ben-Kiki, O., d\u00f6t Net, I., M\u00fcller, T., Antoniou, P., Aro, E., Smith, T.: YAML Ain\u2019t Markup Language (YAML\u2122) Version 1.2 (2021). https:\/\/yaml.org\/spec\/1.2.2\/"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proofs that count. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20\u201321 January 2014, pp. 151\u2013164. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535885","DOI":"10.1145\/2535838.2535885"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Farzan, A., Klumpp, D., Podelski, A.: Sound sequentialization for concurrent program verification. In: Jhala, R., Dillig, I. (eds.) PLDI 2022: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, 13\u201317 June 2022, pp. 506\u2013521. ACM (2022). https:\/\/doi.org\/10.1145\/3519939.3523727","DOI":"10.1145\/3519939.3523727"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Farzan, A., Klumpp, D., Podelski, A.: Commutativity simplifies proofs of parameterized programs. Proc. ACM Program. Lang. 8(POPL), 2485\u20132513 (2024). https:\/\/doi.org\/10.1145\/3632925","DOI":"10.1145\/3632925"},{"issue":"3","key":"4_CR31","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/S10703-016-0243-X","volume":"48","author":"J Filli\u00e2tre","year":"2016","unstructured":"Filli\u00e2tre, J., Gondelman, L., Paskevich, A.: The spirit of ghost code. Formal Methods Syst. Des. 48(3), 152\u2013174 (2016). https:\/\/doi.org\/10.1007\/S10703-016-0243-X","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Fleischmann, M., Kaindlstorfer, D., Isychev, A., W\u00fcstholz, V., Christakis, M.: Constraint-based test oracles for program analyzers. In: Proceedings of the 39th International Conference on Automated Software Engineering (ASE 2024). ACM (2024). https:\/\/doi.org\/10.1145\/3691620.3695035","DOI":"10.1145\/3691620.3695035"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-030-88806-0_6","volume-title":"Static Analysis","author":"L Franceschino","year":"2021","unstructured":"Franceschino, L., Pichardie, D., Talpin, J.-P.: Verified functional programming of an abstract interpreter. In: Dr\u0103goi, C., Mukherjee, S., Namjoshi, K. (eds.) SAS 2021. LNCS, vol. 12913, pp. 124\u2013143. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_6"},{"issue":"12","key":"4_CR34","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1145\/359897.359903","volume":"20","author":"D Gries","year":"1977","unstructured":"Gries, D.: An exercise in proving parallel programs correct. Commun. ACM 20(12), 921\u2013930 (1977). https:\/\/doi.org\/10.1145\/359897.359903","journal-title":"Commun. ACM"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-36577-X_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M.: Proof-like counter-examples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 160\u2013175. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_12"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Haltermann, J., Wehrheim, H.: Information exchange between over- and underapproximating software analyses. In: Schlingloff, B.H., Chai, M. (eds.) Software Engineering and Formal Methods. Lecture Notes in Computer Science, pp. 37\u201354. Springer, Cham (2022). ISBN 978-3-031-17108-6. https:\/\/doi.org\/10.1007\/978-3-031-17108-6_3","DOI":"10.1007\/978-3-031-17108-6_3"},{"key":"4_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-03237-0_7","volume-title":"Static Analysis","author":"M Heizmann","year":"2009","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69\u201385. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03237-0_7"},{"key":"4_CR38","doi-asserted-by":"publisher","unstructured":"Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: a pearl in compositional verification. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 473\u2013485. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009893","DOI":"10.1145\/3009837.3009893"},{"key":"4_CR39","unstructured":"International Organization for Standardization and International Electrotechnical Commission: ISO\/IEC 9899:1999 - Programming Languages - C. Technical report, ISO\/IEC JTC 1\/SC 22 (1999). http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1124.pdf. ISO\/IEC 9899:1999 (C99) draft"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15\u201317 January 2015, pp. 247\u2013259. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676966","DOI":"10.1145\/2676726.2676966"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Kaindlstorfer, D., Isychev, A., W\u00fcstholz, V., Christakis, M.: Interrogation testing of program analyzers for soundness and precision issues. In: Proceedings of the 39th International Conference on Automated Software Engineering (ASE 2024). ACM (2024). https:\/\/doi.org\/10.1145\/3691620.3695034","DOI":"10.1145\/3691620.3695034"},{"issue":"7","key":"4_CR42","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"RM Keller","year":"1976","unstructured":"Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371\u2013384 (1976). https:\/\/doi.org\/10.1145\/360248.360251","journal-title":"Commun. ACM"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Klinger, C., Christakis, M., W\u00fcstholz, V.: Differentially testing soundness and precision of program analyzers. In: Zhang, D., M\u00f8ller, A. (eds.) Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, Beijing, China, 15\u201319 July 2019, pp. 239\u2013250. ACM (2019). https:\/\/doi.org\/10.1145\/3293882.3330553","DOI":"10.1145\/3293882.3330553"},{"key":"4_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-030-99527-0_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Klumpp","year":"2022","unstructured":"Klumpp, D., Dietsch, D., Heizmann, M., Sch\u00fcssele, F., Ebbinghaus, M., Farzan, A., Podelski, A.: Ultimate GemCutter and the axes of generalization. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 479\u2013483. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_35"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-662-54434-1_26","volume-title":"Programming Languages and Systems","author":"R Krebbers","year":"2017","unstructured":"Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 696\u2013723. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26"},{"key":"4_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-662-47666-6_25","volume-title":"Automata, Languages, and Programming","author":"O Lahav","year":"2015","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311\u2013323. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_25"},{"issue":"2","key":"4_CR47","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2), 125\u2013143 (1977). https:\/\/doi.org\/10.1109\/TSE.1977.229904","journal-title":"IEEE Trans. Software Eng."},{"issue":"7","key":"4_CR48","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978). https:\/\/doi.org\/10.1145\/359545.359563","journal-title":"Commun. ACM"},{"issue":"9","key":"4_CR49","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers 28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439","journal-title":"IEEE Trans. Computers"},{"key":"4_CR50","doi-asserted-by":"publisher","unstructured":"Ley-Wild, R., Nanevski, A.: Subjective auxiliary state for coarse-grained concurrency. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy - 23\u201325 January 2013, pp. 561\u2013574. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429134","DOI":"10.1145\/2429069.2429134"},{"key":"4_CR51","doi-asserted-by":"publisher","unstructured":"Lomet, D.B.: Process structuring, synchronization, and recovery using atomic actions. In: Wortman, D.B. (ed.) Proceedings of an ACM Conference on Language Design for Reliable Software (LDRS), Raleigh, North Carolina, USA, 28\u201330 March 1977, pp. 128\u2013137. ACM (1977). https:\/\/doi.org\/10.1145\/800022.808319","DOI":"10.1145\/800022.808319"},{"key":"4_CR52","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"BD Lubachevsky","year":"1984","unstructured":"Lubachevsky, B.D.: An approach to automating the verification of compact parallel coordination programs I. Acta Informatica 21, 125\u2013169 (1984). https:\/\/doi.org\/10.1007\/BF00289237","journal-title":"Acta Informatica"},{"key":"4_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-17906-2_30","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"A Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 278\u2013324. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-17906-2_30"},{"key":"4_CR54","doi-asserted-by":"publisher","unstructured":"McCloskey, B., Zhou, F., Gay, D., Brewer, E.A.: Autolocker: synchronization inference for atomic sections. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, 11\u201313 January 2006, pp. 346\u2013358. ACM (2006). https:\/\/doi.org\/10.1145\/1111037.1111068","DOI":"10.1145\/1111037.1111068"},{"key":"4_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-540-30232-2_17","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"R Meolic","year":"2004","unstructured":"Meolic, R., Fantechi, A., Gnesi, S.: Witness and counterexample automata for ACTL. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 259\u2013275. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30232-2_17"},{"key":"4_CR56","doi-asserted-by":"publisher","unstructured":"Milanese, M., Min\u00e9, A.: Generation of violation witnesses by under-approximating abstract interpretation. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.) Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, 15\u201316 January 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14499, pp. 50\u201373. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-50524-9_3","DOI":"10.1007\/978-3-031-50524-9_3"},{"key":"4_CR57","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Static analysis of run-time errors in embedded real-time parallel C programs. Log. Methods Comput. Sci. 8(1) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(1:26)2012","DOI":"10.2168\/LMCS-8(1:26)2012"},{"key":"4_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-54013-4_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Min\u00e9","year":"2014","unstructured":"Min\u00e9, A.: Relational thread-modular static value analysis by abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 39\u201358. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_3"},{"key":"4_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-52234-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Monat","year":"2017","unstructured":"Monat, R., Min\u00e9, A.: Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 386\u2013404. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_21"},{"key":"4_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-66706-5_13","volume-title":"Static Analysis","author":"S Mukherjee","year":"2017","unstructured":"Mukherjee, S., Padon, O., Shoham, S., D\u2019Souza, D., Rinetzky, N.: Thread-local semantics and its efficient sequential abstractions for race-free programs. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 253\u2013276. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_13"},{"key":"4_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-54833-8_16","volume-title":"Programming Languages and Systems","author":"A Nanevski","year":"2014","unstructured":"Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A.: Communicating state transition systems for fine-grained concurrent resources. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 290\u2013310. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_16"},{"key":"4_CR62","doi-asserted-by":"publisher","unstructured":"Nieto, L.P.: Completeness of the Owicki-Gries system for parameterized parallel programs. In: Proceedings of the 15th International Parallel & Distributed Processing Symposium (IPDPS-01), San Francisco, CA, USA, 23\u201327 April 2001, p. 150. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/IPDPS.2001.925138","DOI":"10.1109\/IPDPS.2001.925138"},{"key":"4_CR63","unstructured":"Nieto, L.P.: Verification of parallel programs with the Owicki-Gries and Rely-Guarantee methods in Isabelle, HOL. Ph.D. thesis, Technical University Munich, Germany (2002). https:\/\/mediatum.ub.tum.de\/?id=601717"},{"key":"4_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-49020-3_13","volume-title":"Fundamental Approaches to Software Engineering","author":"T Nipkow","year":"1999","unstructured":"Nipkow, T., Nieto, L.P.: Owicki\/Gries in Isabelle\/HOL. In: Finance, J.-P. (ed.) FASE 1999. LNCS, vol. 1577, pp. 188\u2013203. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-3-540-49020-3_13"},{"key":"4_CR65","unstructured":"OASIS SARIF Technical Committee: Static analysis results interchange format (SARIF) version 2.1.0. OASIS standard, Organization for the Advancement of Structured Information Standards (OASIS) (2020). https:\/\/docs.oasis-open.org\/sarif\/sarif\/v2.1.0\/os\/sarif-v2.1.0-os.pdf"},{"issue":"5","key":"4_CR66","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279\u2013285 (1976). https:\/\/doi.org\/10.1145\/360051.360224","journal-title":"Commun. ACM"},{"key":"4_CR67","doi-asserted-by":"publisher","unstructured":"Raad, A., Lahav, O., Vafeiadis, V.: Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. Proc. ACM Program. Lang. 4(OOPSLA), 151:1\u2013151:28 (2020). https:\/\/doi.org\/10.1145\/3428219","DOI":"10.1145\/3428219"},{"key":"4_CR68","doi-asserted-by":"publisher","unstructured":"Saan, S., et al.: Goblint: Autotuning thread-modular abstract interpretation. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 547\u2013552. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_34","DOI":"10.1007\/978-3-031-30820-8_34"},{"key":"4_CR69","doi-asserted-by":"publisher","unstructured":"Saan, S., Schwarz, M., Erhard, J., Seidl, H., Tilscher, S., Vojdani, V.: Correctness witness validation by abstract interpretation. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.) Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, 15\u201316 January 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14499, pp. 74\u201397. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-50524-9_4","DOI":"10.1007\/978-3-031-50524-9_4"},{"key":"4_CR70","doi-asserted-by":"publisher","unstructured":"Schmaltz, S.B.: Towards the pervasive formal verification of multi-core operating systems and hypervisors implemented in C. Ph.D. thesis, Universit\u00e4t des Saarlandes (2012). https:\/\/doi.org\/10.22028\/D291-26525","DOI":"10.22028\/D291-26525"},{"key":"4_CR71","doi-asserted-by":"publisher","unstructured":"Schreiber, T.: Auxiliary variables and recursive procedures. In: Bidoit, M., Dauchet, M. (eds.) TAPSOFT\u201997: Theory and Practice of Software Development, 7th International Joint Conference CAAP\/FASE, Lille, France, 14\u201318 April 1997, Proceedings. Lecture Notes in Computer Science, vol. 1214, pp. 697\u2013711. Springer (1997). https:\/\/doi.org\/10.1007\/BFB0030635","DOI":"10.1007\/BFB0030635"},{"key":"4_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-030-88806-0_18","volume-title":"Static Analysis","author":"M Schwarz","year":"2021","unstructured":"Schwarz, M., Saan, S., Seidl, H., Apinis, K., Erhard, J., Vojdani, V.: Improving thread-modular abstract interpretation. In: Dr\u0103goi, C., Mukherjee, S., Namjoshi, K. (eds.) SAS 2021. LNCS, vol. 12913, pp. 359\u2013383. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_18"},{"key":"4_CR73","doi-asserted-by":"publisher","unstructured":"Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V.: Clustered relational thread-modular abstract interpretation with local traces. In: Wies, T. (ed.) Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Paris, France, 22\u201327 April 2023, Proceedings. Lecture Notes in Computer Science, vol. 13990, pp. 28\u201358. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_2","DOI":"10.1007\/978-3-031-30044-8_2"},{"key":"4_CR74","doi-asserted-by":"publisher","unstructured":"Semenyuk, M., Dongol, B.: Ownership-based Owicki-Gries reasoning. In: Hong, J., Lanperne, M., Park, J.W., Cern\u00fd, T., Shahriar, H. (eds.) Proceedings of the 38th ACM\/SIGAPP Symposium on Applied Computing, SAC 2023, Tallinn, Estonia, 27\u201331 March 2023, pp. 1685\u20131694. ACM (2023). https:\/\/doi.org\/10.1145\/3555776.3577636","DOI":"10.1145\/3555776.3577636"},{"key":"4_CR75","doi-asserted-by":"publisher","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15\u201317 June 2015, pp. 77\u201387. ACM (2015). https:\/\/doi.org\/10.1145\/2737924.2737964","DOI":"10.1145\/2737924.2737964"},{"key":"4_CR76","doi-asserted-by":"publisher","unstructured":"Stade, Y., Tilscher, S., Seidl, H.: The top-down solver verified: building confidence in static analyzers. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, 24\u201327 July 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 303\u2013324. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_15","DOI":"10.1007\/978-3-031-65627-9_15"},{"key":"4_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-030-45190-5_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J \u0160vejda","year":"2020","unstructured":"\u0160vejda, J., Berger, P., Katoen, J.-P.: Interpretation-based violation witness validation for C: NITWIT. In: TACAS 2020. LNCS, vol. 12078, pp. 40\u201357. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_3"},{"key":"4_CR78","unstructured":"Ultimate developers: Ultimate program analysis framework (2024). https:\/\/ultimate-pa.org\/. Accessed 29 Sept 2024"},{"key":"4_CR79","doi-asserted-by":"publisher","unstructured":"Vick, C., McMillan, K.L.: Synthesizing history and prophecy variables for symbolic model checking. In: Dragoi, C., Emmi, M., Wang, J. (eds.) Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, 16\u201317 January 2023, Proceedings. Lecture Notes in Computer Science, vol. 13881, pp. 320\u2013340. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_15","DOI":"10.1007\/978-3-031-24950-1_15"},{"key":"4_CR80","doi-asserted-by":"publisher","unstructured":"de\u00a0Vilhena, P.E., Pottier, F., Jourdan, J.: Spy game: verifying a local generic solver in Iris. Proc. ACM Program. Lang. 4(POPL), 33:1\u201333:28 (2020). https:\/\/doi.org\/10.1145\/3371101","DOI":"10.1145\/3371101"},{"key":"4_CR81","doi-asserted-by":"publisher","unstructured":"Vojdani, V., Apinis, K., R\u00f5tov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the Goblint approach. In: Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering. ACM (2016). https:\/\/doi.org\/10.1145\/2970276.2970337","DOI":"10.1145\/2970276.2970337"},{"key":"4_CR82","doi-asserted-by":"publisher","unstructured":"Wright, D., Dalvandi, S., Batty, M., Dongol, B.: Mechanised operational reasoning for C11 programs with relaxed dependencies. Formal Aspects Comput. 35(2), 10:1\u201310:27 (2023). https:\/\/doi.org\/10.1145\/3580285","DOI":"10.1145\/3580285"},{"key":"4_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-29952-0_12","volume-title":"Theory and Applications of Models of Computation","author":"Z Zhang","year":"2012","unstructured":"Zhang, Z., Feng, X., Fu, M., Shao, Z., Li, Y.: A structural approach to prophecy variables. In: Agrawal, M., Cooper, S.B., Li, A. (eds.) TAMC 2012. LNCS, vol. 7287, pp. 61\u201371. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29952-0_12"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-82700-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T01:26:39Z","timestamp":1737595599000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-82700-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031826993","9783031827006"],"references-count":83,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-82700-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"24 January 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denver, CO","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 January 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}