{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T18:52:49Z","timestamp":1773255169270,"version":"3.50.1"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T00:00:00Z","timestamp":1773187200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T00:00:00Z","timestamp":1773187200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Math.Comput.Sci."],"published-print":{"date-parts":[[2026,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Program verification using abstract interpretation involves the symbolic calculation of fixpoints over lattices. Integral to these fixpoint calculations is widening, an operation that trades precision for guarantees of termination. Abstract interpretation often works with lattices of convex sets of points in n-dimensional space, represented by sets of linear inequalities. When the form of these inequalities is restricted these are known as weakly relational domains. This paper addresses weakly relational domains, the detail of their representation and the way in which widening is applied, including study of how the closure operators used in weakly relational domains interact with widening, and considers how sequences of constraints might be widened. Satisfiability checking for numeric constraints is one tool used in this work.<\/jats:p>","DOI":"10.1007\/s11786-025-00612-6","type":"journal-article","created":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:43:58Z","timestamp":1773193438000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Canonical Forms and Widening for Two Variables Per Inequality Systems"],"prefix":"10.1007","volume":"20","author":[{"given":"Martin","family":"Brain","sequence":"first","affiliation":[]},{"given":"Jacob M.","family":"Howe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,3,11]]},"reference":[{"key":"612_CR1","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Program Analysis, pp. 238\u2013252. ACM Press, New York (1977)","DOI":"10.1145\/512950.512973"},{"key":"612_CR2","volume-title":"Principles of Abstract Interpretation","author":"P Cousot","year":"2021","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press, Cambridge (2021)"},{"key":"612_CR3","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages, pp. 84\u201397. ACM Press, New York (1978)","DOI":"10.1145\/512760.512770"},{"key":"612_CR4","doi-asserted-by":"crossref","unstructured":"Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: Logic Based Program Development and Transformation. Lecture Notes in Computer Science, vol. 2664, pp. 71\u201389. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45013-0_7"},{"issue":"1","key":"612_CR5","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"Higher-Order Symb. Comput."},{"key":"612_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2018.12.001","volume":"768","author":"JM Howe","year":"2019","unstructured":"Howe, J.M., King, A., Simon, A.: Incremental closure for systems of two variables per inequality. Theoret. Comput. Sci. 768, 1\u201342 (2019)","journal-title":"Theoret. Comput. Sci."},{"key":"612_CR7","unstructured":"Brain, M., Howe, J.M.: Widening for systems of two variables per inequality. In: Proceedings of the 8th SC-Square Workshop. CEUR Workshop Proceedings, vol. 3455, pp. 11\u201328 (2023)"},{"key":"612_CR8","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/s10990-009-9046-8","volume":"22","author":"D Monniaux","year":"2009","unstructured":"Monniaux, D.: A minimalistic look at widening operators. Higher-Order Symb. Comput. 22, 145\u2013154 (2009)","journal-title":"Higher-Order Symb. Comput."},{"issue":"4","key":"612_CR9","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/s00236-018-0324-y","volume":"56","author":"D Monniaux","year":"2019","unstructured":"Monniaux, D.: On the decidability of the existence of polyhedral invariants in transition systems. Acta Inform. 56(4), 385\u2013389 (2019)","journal-title":"Acta Inform."},{"key":"612_CR10","doi-asserted-by":"crossref","unstructured":"Howe, J.M., King, A.: Logahedra: a new weakly relational domain. In: International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 5799, pp. 306\u2013320. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04761-9_23"},{"key":"612_CR11","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s10703-013-0199-z","volume":"44","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher, T., F\u00fcgger, M., Brauer, J.: Runtime verification of embedded real-time systems. Formal Methods Syst. Des. 44, 203\u2013239 (2014)","journal-title":"Formal Methods Syst. Des."},{"key":"612_CR12","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10703-009-0089-6","volume":"35","author":"P Cousot","year":"2009","unstructured":"Cousot, P., Cousot, R., Feret, J., Min\u00e9, A., Rival, X.: Why does ASTR\u00c9E scale up? Formal Methods Syst. Des. 35, 229\u2013264 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"612_CR13","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Second Symposium on Programs as Data Objects. Lecture Notes in Computer Science, vol. 2053, pp. 155\u2013172. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44978-7_10"},{"issue":"3","key":"612_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3457885","volume":"43","author":"G Gange","year":"2021","unstructured":"Gange, G., Ma, Z., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.: A fresh look at zones and octagons. ACM Trans. Program. Lang. Syst. 43(3), 1\u201351 (2021)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"612_CR15","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming. Lecture Notes in Computer Science, vol. 631, pp. 269\u2013295. Springer, Berlin (1992)","DOI":"10.1007\/3-540-55844-6_142"},{"key":"612_CR16","doi-asserted-by":"crossref","unstructured":"Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Proceedings of the International Conference on Formal Methods in Programming and Their Applications. Lecture Notes in Computer Science, vol. 735, pp. 128\u2013141. Springer, Berlin (1993)","DOI":"10.1007\/BFb0039704"},{"key":"612_CR17","doi-asserted-by":"publisher","unstructured":"Fukuda, K., Prodon, A.: Double description method revisited. In: Combinatorics and Computer Science. Lecture Notes in Computer Science, vol. 1120, pp. 91\u2013111. Springer, Berlin (1995). https:\/\/doi.org\/10.1007\/3-540-61576-8_77","DOI":"10.1007\/3-540-61576-8_77"},{"issue":"1\u20132","key":"612_CR18","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.scico.2005.02.003","volume":"58","author":"R Bagnara","year":"2005","unstructured":"Bagnara, R., Hill, P.M., Mazzi, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1\u20132), 28\u201356 (2005)","journal-title":"Sci. Comput. Program."},{"key":"612_CR19","doi-asserted-by":"publisher","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones. Lecture Notes in Computer Science, vol. 2566, pp. 85\u2013108. Springer, Berlin (2002). https:\/\/doi.org\/10.1007\/3-540-36377-7_5","DOI":"10.1007\/3-540-36377-7_5"},{"key":"612_CR20","doi-asserted-by":"crossref","unstructured":"Simon, A., King, A.: Widening Polyhedra with Landmarks. In: Proceedings of the 4th Asian Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 4279, pp. 166\u2013182. Springer, Berlin (2006)","DOI":"10.1007\/11924661_11"},{"key":"612_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84800-017-9","volume-title":"Value-Range Analysis of C Programs","author":"A Simon","year":"2008","unstructured":"Simon, A.: Value-Range Analysis of C Programs. Springer, Berlin (2008)"},{"key":"612_CR22","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.W.: Lookahead widening. In: Proceedings of the 18th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 4144, pp. 452\u2013466. Springer, Berlin (2006)","DOI":"10.1007\/11817963_41"},{"key":"612_CR23","doi-asserted-by":"crossref","unstructured":"Simon, A., Chen, L.: Simple and precise widenings for polyhedra. In: Proceedings of the 8th Asian Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 6461, pp. 139\u2013155. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-17164-2_11"},{"key":"612_CR24","doi-asserted-by":"crossref","unstructured":"Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Proceedings of the 13th International Static Analysis Symposium. Lecture Notes in Computer Science, vol. 4134, pp. 144\u2013160. Springer, Berlin (2006)","DOI":"10.1007\/11823230_10"},{"key":"612_CR25","doi-asserted-by":"crossref","unstructured":"Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Proceedings of the 22th International Static Analysis Symposium. Lecture Notes in Computer Science, vol. 9291, pp. 145\u2013161. Springer, Berlin (2015)","DOI":"10.1007\/978-3-662-48288-9_9"},{"key":"612_CR26","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-981-19-9601-6_4","volume-title":"Challenges of Software Verification. Intelligent Systems Reference Library","author":"E Zaffanella","year":"2023","unstructured":"Zaffanella, E., Arceri, V.: \u201cFixing\u2019\u2019 the specification of widenings. In: Arceri, V., Cortesi, A., Ferrara, P., Olliaro, M. (eds.) Challenges of Software Verification. Intelligent Systems Reference Library, vol. 238, pp. 57\u201376. Springer, Berlin (2023)"},{"key":"612_CR27","doi-asserted-by":"crossref","unstructured":"Ballou, K., Sherman, E.: Incremental transitive closure for zonal abstract domain. In: Proceedings of the 14th International Symposium NASA Formal Methods. Lecture Notes in Computer Science, vol. 13260, pp. 800\u2013808. Springer, Berlin (2022)","DOI":"10.1007\/978-3-031-06773-0_43"},{"key":"612_CR28","doi-asserted-by":"crossref","unstructured":"Gange, G., Navas, A. J, Schachte, P., S\u00f8ndergaard, H., Stuckey, P.: Dissecting widening: separating termination from information. In: Proceedings of the 17th Asian Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 11893, pp. 95\u2013114. Springer, Berlin (2019)","DOI":"10.1007\/978-3-030-34175-6_6"},{"key":"612_CR29","doi-asserted-by":"crossref","unstructured":"Bagnara, R., Hill, P.M., Mazzi, E., Zaffanella, E.: Widening operators for weakly-relational numeric abstractions. In: Proceedings of the 12th International Symposium on Static Analysis. Lecture Notes in Computer Science, vol. 3672, pp. 3\u201318. Springer, Berlin (2005)","DOI":"10.1007\/11547662_3"},{"issue":"3","key":"612_CR30","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10703-009-0073-1","volume":"35","author":"R Bagnara","year":"2009","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness. Formal Methods Syst. Des. 35(3), 279\u2013323 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"612_CR31","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Dang, T., Ivan\u010di\u0107, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Tools and algorithms for the construction and analysis of systems. Lecture Notes in Computer Science, vol. 4963, pp. 188\u2013202. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_14"},{"key":"612_CR32","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Col\u00f3n, M.A., Sipma, H., Manna, Z.: Efficient strongly relational polyhedral analysis. In: Verification, model checking, and abstract interpretation. Lecture Notes in Computer Science, vol. 3855, pp. 111\u2013125. Springer, Berlin (2006)","DOI":"10.1007\/11609773_8"},{"key":"612_CR33","doi-asserted-by":"publisher","unstructured":"Feret, J.: Static analysis of digital filters. In: Proceedings of the 13th European Symposium on Programming. Lecture Notes in Computer Science, vol. 2986, pp. 33\u201348. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/11609773_8","DOI":"10.1007\/11609773_8"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-025-00612-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11786-025-00612-6","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-025-00612-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:44:01Z","timestamp":1773193441000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11786-025-00612-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,11]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,12]]}},"alternative-id":["612"],"URL":"https:\/\/doi.org\/10.1007\/s11786-025-00612-6","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"value":"1661-8270","type":"print"},{"value":"1661-8289","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,11]]},"assertion":[{"value":"29 February 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 January 2025","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 January 2025","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 March 2026","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing Interests"}}],"article-number":"2"}}