{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T11:16:29Z","timestamp":1783509389607,"version":"3.55.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986819","type":"print"},{"value":"9783031986826","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We consider the use of commutativity-based reduction for the algorithmic verification of concurrent programs. In existing work, the commutativity relation used for the reduction is mostly fixed statically. In this paper, we propose a\n                    <jats:italic>demand-driven<\/jats:italic>\n                    approach to compute the commutativity relation. The approach can be viewed as the direct analogue of the CEGAR approach which uses counterexamples to guide the incremental refinement of the abstraction. Instead of eliminating a counterexample by proving it infeasible and refining the abstraction, we can eliminate a counterexample by proving it\n                    <jats:italic>redundant<\/jats:italic>\n                    and expanding the commutativity relation. When we prove a counterexample redundant, we use the proof for a generalization step which allows us to eliminate not just a single counterexample, but a whole infinite set. We present a general scheme where we integrate the new approach with the CEGAR approach. We have implemented an instantiation of the general scheme. An experimental evaluation shows an increase in the number of successfully verified programs by 15% on a challenging benchmark set.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_18","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:14:28Z","timestamp":1753154068000},"page":"347-369","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Counterexample-Guided Commutativity"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-9216-1801","authenticated-orcid":false,"given":"Marcel","family":"Ebbinghaus","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4885-0728","authenticated-orcid":false,"given":"Dominik","family":"Klumpp","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":[[2025,7,23]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Jonsson, B., Kindahl, M., Peled, D.A.: A general approach to partial order reductions in symbolic verification (extended abstract). In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification, 10th International Conference, CAV 1998, Vancouver, BC, Canada, 28 June\u20132 July 1998, Proceedings. Lecture Notes in Computer Science, vol.\u00a01427, pp. 379\u2013390. Springer (1998). https:\/\/doi.org\/10.1007\/BFB0028760","DOI":"10.1007\/BFB0028760"},{"key":"18_CR2","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"issue":"7","key":"18_CR3","doi-asserted-by":"publisher","first-page":"1333","DOI":"10.1007\/S10817-020-09573-W","volume":"64","author":"K Bansal","year":"2020","unstructured":"Bansal, K., Koskinen, E., Tripp, O.: Synthesizing precise and useful commutativity conditions. J. Autom. Reason. 64(7), 1333\u20131359 (2020). https:\/\/doi.org\/10.1007\/S10817-020-09573-W","journal-title":"J. Autom. Reason."},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-662-48899-7_17","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Cassez","year":"2015","unstructured":"Cassez, F., Ziegler, F.: Verification of concurrent programs using trace abstraction refinement. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 233\u2013248. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_17"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Chen, A., Fathololumi, P., Nicola, M., Pincus, J., Brennan, T., Koskinen, E.: Better predicates and heuristics for improved commutativity synthesis. In: Andr\u00e9, \u00c9., Sun, J. (eds.) Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, 24\u201327 October 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 14216, pp. 93\u2013113. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_5","DOI":"10.1007\/978-3-031-45332-8_5"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-319-13338-6_14","volume-title":"Hardware and Software: Verification and Testing","author":"D-H Chu","year":"2014","unstructured":"Chu, D.-H., Jaffar, J.: A framework to synergize partial order reduction with state interpolation. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 171\u2013187. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_14"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Heizmann, M., Musa, B., Nutz, A., Podelski, A.: Craig vs. Newton in software model checking. In: Bodden, E., Sch\u00e4fer, W., van Deursen, A., Zisman, A. (eds.) Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2017, Paderborn, Germany, 4\u20138 September 2017, pp. 487\u2013497. ACM (2017). https:\/\/doi.org\/10.1145\/3106237.3106307","DOI":"10.1145\/3106237.3106307"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1007\/978-3-642-39799-8_46","volume-title":"Computer Aided Verification","author":"I Dillig","year":"2013","unstructured":"Dillig, I., Dillig, T.: Explain: a tool for performing abductive inference. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 684\u2013689. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_46"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-15769-1_15","volume-title":"Static Analysis","author":"I Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Small formulas for large programs: on-line constraint simplification in scalable static analysis. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 236\u2013252. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_15"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-642-31424-7_30","volume-title":"Computer Aided Verification","author":"I Dillig","year":"2012","unstructured":"Dillig, I., Dillig, T., McMillan, K.L., Aiken, A.: Minimum satisfying assignments for SMT. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 394\u2013409. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_30"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Ebbinghaus, M., Klumpp, D., Podelski, A.: Artifact for CAV\u201925 Paper \u201cCounterexample-Guided Commutativity\u201d (2025). https:\/\/doi.org\/10.5281\/zenodo.15198876","DOI":"10.5281\/zenodo.15198876"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, 21\u201323 January 2009, pp. 2\u201315. ACM (2009). https:\/\/doi.org\/10.1145\/1480881.1480885","DOI":"10.1145\/1480881.1480885"},{"key":"18_CR13","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":"18_CR14","doi-asserted-by":"publisher","unstructured":"Farzan, A., Klumpp, D., Podelski, A.: Stratified commutativity in verification algorithms for concurrent programs. Proc. ACM Program. Lang. 7(POPL), 1426\u20131453 (2023). https:\/\/doi.org\/10.1145\/3571242","DOI":"10.1145\/3571242"},{"key":"18_CR15","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"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-030-25540-4_11","volume-title":"Computer Aided Verification","author":"A Farzan","year":"2019","unstructured":"Farzan, A., Vandikas, A.: Automated hypersafety verification. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 200\u2013218. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_11"},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"Farzan, A., Vandikas, A.: Reductions for safety proofs. Proc. ACM Program. Lang. 4(POPL), 13:1\u201313:28 (2020). https:\/\/doi.org\/10.1145\/3371081","DOI":"10.1145\/3371081"},{"key":"18_CR18","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":"18_CR19","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":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Klumpp, D., Nitzke, L., Sch\u00fcssele, F.: Petrification: software model checking for programs with dynamic thread management. 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 II. Lecture Notes in Computer Science, vol. 14500, pp. 3\u201325. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-50521-8_1","DOI":"10.1007\/978-3-031-50521-8_1"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-02658-4_31","volume-title":"Computer Aided Verification","author":"V Kahlon","year":"2009","unstructured":"Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 398\u2013413. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_31"},{"key":"18_CR23","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., et al.: 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":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-030-67067-2_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Koskinen","year":"2021","unstructured":"Koskinen, E., Bansal, K.: Decomposing data structure commutativity proofs with $$m\\!n$$-differencing. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 81\u2013103. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_5"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-96145-3_5","volume-title":"Computer Aided Verification","author":"B Kragl","year":"2018","unstructured":"Kragl, B., Qadeer, S.: Layered concurrent programs. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 79\u2013102. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_5"},{"key":"18_CR26","unstructured":"Leino, K.R.M.: This is Boogie 2 (2008). https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"issue":"12","key":"18_CR27","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975). https:\/\/doi.org\/10.1145\/361227.361234","journal-title":"Commun. ACM"},{"key":"18_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/3-540-58179-0_69","volume-title":"Computer Aided Verification","author":"D Peled","year":"1994","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377\u2013390. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_69"},{"key":"18_CR29","unstructured":"Vandikas, A., Farzan, A.: Example programs for the Weaver verifier (2021). https:\/\/github.com\/weaver-verifier\/weaver\/tree\/master\/examples"},{"key":"18_CR30","doi-asserted-by":"publisher","unstructured":"Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with Impact. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp. 210\u2013217. IEEE (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679412","DOI":"10.1109\/FMCAD.2013.6679412"}],"updated-by":[{"DOI":"10.1007\/978-3-031-98682-6_22","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T00:00:00Z","timestamp":1760054400000}}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98682-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T10:32:11Z","timestamp":1783506731000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_18","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":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"10 October 2025","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"A correction has been published.","order":4,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","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":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}