{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:43:03Z","timestamp":1770291783226,"version":"3.49.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>Many algorithms in verification and automated reasoning leverage some form of duality between proofs and refutations or counterexamples. In most cases, duality is only used as an intuition that helps in understanding the algorithms and is not formalized. In other cases, duality is used explicitly, but in a specially tailored way that does not generalize to other problems.<\/jats:p>\n                  <jats:p>In this paper we propose a unified primal-dual framework for designing verification algorithms that leverage duality. To that end, we generalize the concept of a Lagrangian that is commonly used in linear programming and optimization to capture the domains considered in verification problems, which are usually discrete, e.g., powersets of states, predicates, ranking functions, etc. A Lagrangian then induces a primal problem and a dual problem. We devise an abstract primal-dual procedure that simultaneously searches for a primal solution and a dual solution, where the two searches guide each other. We provide sufficient conditions that ensure that the procedure makes progress under certain monotonicity assumptions on the Lagrangian.<\/jats:p>\n                  <jats:p>We show that many existing algorithms in program analysis, verification, and automated reasoning can be derived from our algorithmic framework with a suitable choice of Lagrangian. The Lagrangian-based formulation sheds new light on various characteristics of these algorithms, such as the ingredients they use to ensure monotonicity and guarantee progress. We further use our framework to develop a new validity checking algorithm for fixpoint logic over quantified linear arithmetic. Our prototype achieves promising results and in some cases solves instances that are not solved by state-of-the-art techniques.<\/jats:p>","DOI":"10.1145\/3704904","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"2025-2056","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Primal-Dual Perspective on Program Verification Algorithms"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"Takeshi","family":"Tsukada","sequence":"first","affiliation":[{"name":"Chiba University, Chiba, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[{"name":"Tohoku University, Sendai, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4209-1635","authenticated-orcid":false,"given":"Oded","family":"Padon","sequence":"additional","affiliation":[{"name":"Weizmann Institute of Science, Rehovot, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Thomas Ball Rupak Majumdar Todd D. Millstein and Sriram K. Rajamani. 2001a. Automatic Predicate Abstraction of C Programs. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) Snowbird Utah USA June 20-22 2001 Michael Burke and Mary Lou Soffa (Eds.). ACM 203\u2013213. https:\/\/doi.org\/10.1145\/378795.378846 10.1145\/378795.378846","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_19"},{"key":"e_1_3_2_4_1","article-title":"Athena scientific optimization and computation series","volume":"6","author":"Bertsimas Dimitris","year":"1997","unstructured":"Dimitris Bertsimas and John N. Tsitsiklis. 1997. Introduction to linear optimization. Athena scientific optimization and computation series, Vol. 6. Athena Scientific.","journal-title":"Introduction to linear optimization"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Nikolaj Bj\u00f8rner and Mikol\u00e1\u0161 Janota. 2015. Playing with Quantified Satisfaction. In 20th International Conferences on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2015) (EPiC Series in Computing). Easy Chair. https:\/\/doi.org\/10.29007\/vv21 10.29007\/vv21","DOI":"10.29007\/vv21"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38499-8_5"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_8"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","unstructured":"Byron Cook Andreas Podelski and Andrey Rybalchenko. 2006. Termination proofs for systems code. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201906). ACM 415\u2013426. https:\/\/doi.org\/10.1145\/1133981.1134029 10.1145\/1133981.1134029","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_15_1","unstructured":"Niklas Een Alan Mishchenko and Robert Brayton. 2011. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD). 125\u2013134."},{"key":"e_1_3_2_16_1","first-page":"9","volume-title":"Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016","author":"Farzan Azadeh","year":"2016","unstructured":"Azadeh Farzan and Zachary Kincaid. 2016. Linear Arithmetic Satisfiability via Strategy Improvement. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9\u201315 July 2016, Subbarao Kambhampati (Ed.). IJCAI\/AAAI Press, 735\u2013743. http:\/\/www.ijcai.org\/Abstract\/16\/110"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158149"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00196-4"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","unstructured":"Patrice Godefroid Aditya V. Nori Sriram K. Rajamani and Sai Deep Tetali. 2010. Compositional may-must program analysis: unleashing the power of alternation. In Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL \u201910). ACM. https:\/\/doi.org\/10.1145\/1706299.1706307 10.1145\/1706299.1706307","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Laure Gonnord David Monniaux and Gabriel Radanne. 2015. Synthesis of ranking functions using extremal counterexamples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201915). ACM 608\u2013618. https:\/\/doi.org\/10.1145\/2737924.2737976 10.1145\/2737924.2737976","DOI":"10.1145\/2737924.2737976"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632899"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1002\/9781118033036"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11757375_3"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Susmit Jha Sumit Gulwani Sanjit A. Seshia and Ashish Tiwari. 2010. Oracle-guided component-based program synthesis. In Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering - Volume 1 ICSE 2010 Cape Town South Africa 1-8 May 2010 Jeff Kramer Judith Bishop Premkumar T. Devanbu and Sebasti\u00e1n Uchitel (Eds.). ACM 215\u2013224. https:\/\/doi.org\/10.1145\/1806799.1806833 10.1145\/1806799.1806833","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/fmcad.2015.7542257"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_4"},{"key":"e_1_3_2_33_1","doi-asserted-by":"crossref","unstructured":"Xie Li Yi Li Yong Li Xuechao Sun Andrea Turrini and Lijun Zhang. 2020. SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM. ACM 1635\u20131639.","DOI":"10.1145\/3368089.3417930"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_5"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498712"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","unstructured":"A. Podelski and A. Rybalchenko. 2004. Transition invariants. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004). IEEE. https:\/\/doi.org\/10.1109\/lics.2004.1319598 10.1109\/lics.2004.1319598","DOI":"10.1109\/lics.2004.1319598"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498725"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656457"},{"key":"e_1_3_2_40_1","doi-asserted-by":"crossref","unstructured":"Takeshi Tsukada Hiroshi Unno Oded Padon and Sharon Shoham. 2024. A Primal-Dual Perspective on Program Verification Algorithms (extended version). (2024). Available on arXiv.","DOI":"10.1145\/3704904"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571265"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","unstructured":"Hari Govind Vediramana Krishnan YuTing Chen Sharon Shoham and Arie Gurfinkel. 2023. Global guidance for local generalization in model checking. Formal Methods in System Design (March 2023). https:\/\/doi.org\/10.1007\/s10703-023-00412-3 10.1007\/s10703-023-00412-3","DOI":"10.1007\/s10703-023-00412-3"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704904","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704904","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:53Z","timestamp":1770200273000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704904"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704904"],"URL":"https:\/\/doi.org\/10.1145\/3704904","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}