{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:06:29Z","timestamp":1784797589895,"version":"3.55.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Lagrangian-based duality, traditionally applied in optimization, has recently been generalized to serve as the basis for a unifying framework for primal-dual search algorithms in the context of program verification and automated reasoning. In this paper, we analyze Quantified Satisfiability Modulo Theories (QSMT) algorithms using this framework. Interestingly, our Lagrangian-based analysis reveals that three recently proposed algorithms for quantified linear real arithmetic (LRA) share a common structure, and that their main differences lie in the approach to a certain problem\u2014model-based projection for\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\exists \\forall $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mo>\u2203<\/mml:mo>\n                            <mml:mo>\u2200<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -formulas. Moreover, in the course of this Lagrangian-based analysis, we identify an issue with the progress property of one of the algorithms, propose a way to fix the issue, and experimentally demonstrate that the proposed fix improves performance.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_4","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:47:18Z","timestamp":1784796438000},"page":"75-96","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Lagrangian-Based Duality for\u00a0Quantified SMT Algorithms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9984-995X","authenticated-orcid":false,"given":"Ivana","family":"Bocevska","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4209-1635","authenticated-orcid":false,"given":"Oded","family":"Padon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Burke, M., Soffa, M.L. (eds.) Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20-22, 2001, pp. 203\u2013213. ACM (2001). https:\/\/doi.org\/10.1145\/378795.378846","DOI":"10.1145\/378795.378846"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., Janota, M.: Playing with quantified satisfaction. In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A. (eds.) LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations. EPiC Series in Computing, vol.\u00a035, pp. 15\u201327. EasyChair (2015). https:\/\/doi.org\/10.29007\/vv21","DOI":"10.29007\/vv21"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Bocevska, I., Tsukada, T., Unno, H., Padon, O., Shoham, S.: Lagrangian-based duality for quantified smt algorithms - artifact (2026). https:\/\/doi.org\/10.5281\/zenodo.19682202","DOI":"10.5281\/zenodo.19682202"},{"key":"4_CR4","unstructured":"Bocevska, I., Tsukada, T., Unno, H., Padon, O., Shoham, S.: Lagrangian-based duality for quantified SMT algorithms (extended version). In: Proceedings of the 38th International Conference on Computer Aided Verification (CAV). Lisbon, Portugal (July 2026). https:\/\/hal.science\/hal-05623727, hAL Id: hal-05623727"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Vauthier, C.: QSMA: A new algorithm for quantified satisfiability modulo theory and assignment. In: CADE-29, pp. 78\u201395. Springer-Verlag, Berlin, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_5","DOI":"10.1007\/978-3-031-38499-8_5"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Vauthier, C.: The QSMA algorithm for quantifiers in SMT. J. Autom. Reason. 69(2) (May 2025). https:\/\/doi.org\/10.1007\/s10817-025-09727-8","DOI":"10.1007\/s10817-025-09727-8"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Lecture Notes in Computer Science, pp. 70\u201387. Springer Berlin Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, E.K., Karrabi, M., Motwani, H.J., Seeliger, M., \u017dikeli\u0107, u.: Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. In: Proceedings of the Thirty-Ninth AAAI Conference on Artificial Intelligence and Thirty-Seventh Conference on Innovative Applications of Artificial Intelligence and Fifteenth Symposium on Educational Advances in Artificial Intelligence. AAAI\u201925\/IAAI\u201925\/EAAI\u201925, AAAI Press (2025). https:\/\/doi.org\/10.1609\/aaai.v39i11.33213","DOI":"10.1609\/aaai.v39i11.33213"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15\u201319, 2000, Proceedings. Lecture Notes in Computer Science, vol.\u00a01855, pp. 154\u2013169. Springer (2000). https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"key":"4_CR10","unstructured":"Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, pp. 125\u2013134. FMCAD \u201911, FMCAD Inc, Austin, Texas (2011). https:\/\/dl.acm.org\/doi\/10.1145\/3798200"},{"key":"4_CR11","unstructured":"Farzan, A., Kincaid, Z.: Linear arithmetic satisfiability via strategy improvement. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, pp. 735\u2013743. IJCAI\u201916, AAAI Press (2016). https:\/\/dl.acm.org\/doi\/10.5555\/3060621.3060724"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE: A robust framework for learning invariants. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08559, pp. 69\u201387. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Janota, M.: Circuit-based search space pruning in QBF. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9\u201312, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10929, pp. 187\u2013198. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_12","DOI":"10.1007\/978-3-319-94144-8_12"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Tanahashi, K., Sato, R., Tsukada, T.: Hfl(z) validity checking for automated program verification. Proc. ACM Program. Lang. 7(POPL) (Jan 2023). https:\/\/doi.org\/10.1145\/3571199","DOI":"10.1145\/3571199"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Computer Aided Verification (CAV), pp. 17\u201334. Springer International Publishing (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2","DOI":"10.1007\/978-3-319-08867-9_2"},{"issue":"3","key":"4_CR16","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Design 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Methods Syst. Design"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Kura, S., Unno, H., Tsukada, T.: Supermartingales for unique fixed points: A unified approach to lower bound verification (2026). https:\/\/doi.org\/10.48550\/arXiv.2504.04132","DOI":"10.48550\/arXiv.2504.04132"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Murphy, C., Kincaid, Z.: Quantified linear arithmetic satisfiability via fine-grained strategy improvement. In: Computer Aided Verification: 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24\u201327, 2024, Proceedings, Part I, pp. 89\u2013109. Springer-Verlag, Berlin, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_5","DOI":"10.1007\/978-3-031-65627-9_5"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Reynolds, A., King, T., Kuncak, V.: An instantiation-based approach for solving quantified linear arithmetic. CoRR abs\/1510.02642 (2015). https:\/\/doi.org\/10.48550\/arXiv.1510.02642","DOI":"10.48550\/arXiv.1510.02642"},{"issue":"4","key":"4_CR20","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1017\/S1471068417000175","volume":"17","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Tinelli, C., Barrett, C.: Constraint solving for finite model finding in SMT solvers. Theory Pract. Logic Program. 17(4), 516\u2013558 (2017). https:\/\/doi.org\/10.1017\/S1471068417000175","journal-title":"Theory Pract. Logic Program."},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Tsukada, T., Unno, H., Padon, O., Shoham, S.: A primal-dual perspective on program verification algorithms. Proc. ACM Program. Lang. 9(POPL) (Jan 2025). https:\/\/doi.org\/10.1145\/3704904","DOI":"10.1145\/3704904"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Unno, H., Terauchi, T., Gu, Y., Koskinen, E.: Modular primal-dual fixpoint logic solving for temporal verification. Proc. ACM Program. Lang. 7(POPL) (Jan 2023). https:\/\/doi.org\/10.1145\/3571265","DOI":"10.1145\/3571265"}],"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-032-32526-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:47:21Z","timestamp":1784796441000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","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","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}