{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T17:32:30Z","timestamp":1780680750665,"version":"3.54.1"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T00:00:00Z","timestamp":1715558400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T00:00:00Z","timestamp":1715558400000},"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":["Acta Informatica"],"published-print":{"date-parts":[[2024,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Invariant relations are used to analyze while loops; while their primary application is to derive the function of a loop, they can also be used to derive loop invariants, weakest preconditions, strongest postconditions, sufficient conditions of correctness, necessary conditions of correctness, and termination conditions of loops. In this paper we present two generic invariant relations that capture the semantics of loops whose loop body applies affine transformations on numeric variables.<\/jats:p>","DOI":"10.1007\/s00236-024-00457-9","type":"journal-article","created":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T03:14:32Z","timestamp":1715570072000},"page":"261-314","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Invariant relations for affine loops"],"prefix":"10.1007","volume":"61","author":[{"given":"Wided","family":"Ghardallou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hessamaldin","family":"Mohammadi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard C.","family":"Linger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark","family":"Pleszkoch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JiMeng","family":"Loh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6578-5510","authenticated-orcid":false,"given":"Ali","family":"Mili","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,5,13]]},"reference":[{"issue":"1","key":"457_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2010.09.002","volume":"267","author":"C Ancourt","year":"2010","unstructured":"Ancourt, C., Coelho, F., Irigoin, F.: A modular static analysis approach to affine loop invariants detection. Electron. Notes Theor. Comput. Sci. 267(1), 3\u201316 (2010)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"457_CR2","volume-title":"Relational Methods in Computer Science. Advances in Computer Science","author":"C Brink","year":"1997","unstructured":"Brink, C., Kahl, W., Schmidt, G.: Relational Methods in Computer Science. Advances in Computer Science. Springer, Berlin (1997)"},{"key":"457_CR3","doi-asserted-by":"crossref","unstructured":"Carbolnell, E.R., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: Proceedings, ISSAC, pp. 266\u2013273 (2004)","DOI":"10.1145\/1005285.1005324"},{"key":"457_CR4","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1007\/s10009-022-00676-w","volume":"24","author":"S Chakraborty","year":"2022","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Full program induction: verifying array programs sans loop invariants. Int. J. Softw. Tools Technol. Transf. 24, 843\u2013888 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"457_CR5","doi-asserted-by":"crossref","unstructured":"Colon, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Proceedings, CAV 2003, vol. 2725 (2003)","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"457_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages, pp. 84\u201397 (1978)","DOI":"10.1145\/512760.512770"},{"key":"457_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. In: Proceedings of the 1977 Symposium on Artificial Intelligence and Programming Languages. ACM (1977)","DOI":"10.1145\/800228.806926"},{"key":"457_CR8","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/0304-3975(93)90074-4","volume":"114","author":"J Desharnais","year":"1993","unstructured":"Desharnais, J., Jaoua, A., Mili, F., Boudriga, N., Mili, A.: A relational division operator: the conjugate kernel. Theor. Comput. Sci. 114, 247\u2013272 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"457_CR9","unstructured":"Desharnais, J.: Private correspondence. Technical report, Laval University, Quebec City, Canada, April (2023)"},{"key":"457_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlamp.2018.02.001","volume":"97","author":"N Diallo","year":"2018","unstructured":"Diallo, N., Ghardallou, W., Desharnais, J., Mili, A.: Convergence: integrating termination and abort freedom. J. Log. Algebraic Methods Program. 97, 1\u201329 (2018)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"1","key":"457_CR11","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tscantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"457_CR12","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: Proceedings, Formal Methods in Computer Aided Design, pp. 57\u201364 (2015)","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"457_CR13","doi-asserted-by":"crossref","unstructured":"Frohn, F., Hark, M., Giesl, J.: Termination of polynomial loops. In: Proceedings, International Static Analysis Symposium, pp. 89\u2013112 (2020)","DOI":"10.1007\/978-3-030-65474-0_5"},{"key":"457_CR14","doi-asserted-by":"crossref","unstructured":"Furia, C.A., Meyer, B.: Inferring loop invariants using postconditions. In: Dershowitz, N. (ed.) Festschrift in Honor of Yuri Gurevich\u2019s 70th Birthday, Lecture Notes in Computer Science. Springer (2010)","DOI":"10.1007\/978-3-642-15025-8_15"},{"key":"457_CR15","doi-asserted-by":"crossref","unstructured":"Gadelha, M., Monteiro, F., Cordeiro, L., Nicole, D.: Esbmc v6.0: verifying c programs using k-induction and invariant inference. In: Proceedings, International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer (2019)","DOI":"10.1007\/978-3-030-17502-3_15"},{"key":"457_CR16","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Furia, C.A., May, E., Fraser, G., Zeller, A.: Dynamate: dynamically inferring loop invariants for automatic full functional verification. In: Proceedings, HVC 2014, pp. 48\u201353 (2014)","DOI":"10.1007\/978-3-319-13338-6_4"},{"key":"457_CR17","unstructured":"Ghardallou, W.: Analyse de boucles while au moyen de relations invariantes. Technical report, University of Tunis El Manar (2015)"},{"key":"457_CR18","doi-asserted-by":"crossref","unstructured":"Ghardallou, W., Diallo, N., Mili, A., Frias, M.: Debugging without testing. In: Proceedings, International Conference on Software Testing, Chicago, IL, April (2016)","DOI":"10.1109\/ICST.2016.12"},{"issue":"5","key":"457_CR19","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1016\/j.jlap.2012.04.001","volume":"81","author":"W Ghardallou","year":"2012","unstructured":"Ghardallou, W., Mraihi, O., Louhichi, A., Jilani, L.L., Bsaies, K., Mili, A.: A versatile concept for the analysis of loops. J. Log. Algebraic Program. 81(5), 606\u2013622 (2012)","journal-title":"J. Log. Algebraic Program."},{"key":"457_CR20","unstructured":"Gonnord, L.: Acceleration abstraite pour l\u2019amelioration de la precision en analyse des relations lineaires. Technical report, Universite Joseph Fourier de Grenoble (2007)"},{"key":"457_CR21","doi-asserted-by":"crossref","unstructured":"Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Proceedings, SAS 2006, pp. 144\u2013160. Seoul (2006)","DOI":"10.1007\/11823230_10"},{"key":"457_CR22","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.scico.2013.09.016","volume":"93","author":"L Gonnord","year":"2014","unstructured":"Gonnord, L., Schrammel, P.: Abstract acceleration in linear relation analysis. Sci. Comput. Program. 93, 125\u2013153 (2014)","journal-title":"Sci. Comput. Program."},{"key":"457_CR23","doi-asserted-by":"crossref","unstructured":"Gupta, A., Rybalchenko, A.: Invgen: an efficient invariant generator. In: Proceedings, CAV 2009, pp. 634\u2013640 (2009)","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"457_CR24","doi-asserted-by":"crossref","unstructured":"Henzinger, Th. A., Hottelier, Th., Kovacs, L.: Valigator: verification tool with bound and invariant generation. In: Proceedings, LPAR08: International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, Doha, Qatar, November (2008)","DOI":"10.1007\/978-3-540-89439-1_24"},{"key":"457_CR25","doi-asserted-by":"crossref","unstructured":"Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: Polynomial invariants for affine programs. In: Proceedings, Logic in Computer Science, Oxford, UK, July 9\u201312 (2018)","DOI":"10.1145\/3209108.3209142"},{"key":"457_CR26","doi-asserted-by":"crossref","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Automated generation of non-linear loop invariants utilizing hypergeometric sequences. In: Proceedings, ISSAC 2017, Kaiserslautern, Germany (2017)","DOI":"10.1145\/3087604.3087623"},{"key":"457_CR27","doi-asserted-by":"crossref","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Invariant generation for multi-path loops with polynomial assignments. In: Proceedings, VMCAI 2018, pp. 226\u2013246, Los Angeles, CA, USA (2018)","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"457_CR28","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: Proceedings, POPL\u201914, San Diego, CA, January 22\u201324 (2014)","DOI":"10.1145\/2535838.2535843"},{"key":"457_CR29","doi-asserted-by":"crossref","unstructured":"Ji, Y., Fu, H., Fang, B., Chen, H.: Affine loop invariant generation using matrix algebra. In: Proceedings, CAV 2022, pp. 257\u2013281 (2022)","DOI":"10.1007\/978-3-031-13185-1_13"},{"issue":"3","key":"457_CR30","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s11334-012-0189-0","volume":"8","author":"LL Jilani","year":"2012","unstructured":"Jilani, L.L., Louhich, A., Mraihi, O., Mili, A.: Invariant relations, invariant functions and loop functions. Innov. Syst. Softw. Eng. NASA J. 8(3), 195\u2013212 (2012)","journal-title":"Innov. Syst. Softw. Eng. NASA J."},{"key":"457_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jsc.2012.04.001","volume":"48","author":"LL Jilani","year":"2013","unstructured":"Jilani, L.L., Mraihi, O., Louhichi, A., Ghardallou, W., Bsaies, K., Mili, A.: Invariant relations and invariant functions: an alternative to invariant assertions. J. Symb. Comput. 48, 1\u201336 (2013)","journal-title":"J. Symb. Comput."},{"key":"457_CR32","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Inform. 6, 133\u2013151 (1976)","journal-title":"Acta Inform."},{"key":"457_CR33","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Breck, J., Forouhi Boroujeni, A., Reps, T.: Compositional recurrence analysis revisited. In: Proceedings, PLDI (2017)","DOI":"10.1145\/3062341.3062373"},{"key":"457_CR34","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Breck, J., Cyphert, J., Reps, T.: Closed forms for numerical loops. In: Proceedings, Principles of Programming Languages. ACM (2019)","DOI":"10.1145\/3290368"},{"key":"457_CR35","doi-asserted-by":"crossref","unstructured":"Kincaid, Z, Cyphert, J., Breck, J., Reps, T.: Non-linear reasoning for invariant synthesis. In: Proceedings, Principles of Programming Languages, vol. 2. ACM (2018)","DOI":"10.1145\/3158142"},{"issue":"7","key":"457_CR36","doi-asserted-by":"publisher","first-page":"653","DOI":"10.3103\/S0146411619070101","volume":"53","author":"DA Kondratyev","year":"2019","unstructured":"Kondratyev, D.A., Maryasov, I.V., Nepomniaschy, V.A.: The automation of c program verification by the symbolic method of loop invariant elimination. Autom. Control. Comput. Sci. 53(7), 653\u2013662 (2019)","journal-title":"Autom. Control. Comput. Sci."},{"key":"457_CR37","doi-asserted-by":"crossref","unstructured":"Kovacs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Proceedings, 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, September (2009)","DOI":"10.1109\/SYNASC.2009.66"},{"key":"457_CR38","doi-asserted-by":"crossref","unstructured":"Kovacs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Proceedings, FASE 2009, pp. 470\u2013485. LNCS 5503. Springer(2009)","DOI":"10.1007\/978-3-642-00593-0_33"},{"key":"457_CR39","unstructured":"Kovacs, L.: Aligator: a mathematica package for invariant generation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR, Number 5195 in LNCS, pp. 275\u2013282, Sydney, Australia, August. Springer (2008)"},{"key":"457_CR40","unstructured":"Kovacs, L.: Reasoning algebraically about p-solvable loops. In: Proceedings, TACAS (2008)"},{"key":"457_CR41","unstructured":"Kroening, D., Sharygina, N., Tonetta, S., Letychevskyy Jr, A., Potiyenko, S., Weigert, T.: Loopfrog: loop summarization for static analysis. In: Proceedings, Workshop on Invariant Generation: WING 2010, Edinburgh, UK, July (2010)"},{"key":"457_CR42","doi-asserted-by":"crossref","unstructured":"Kroening, D., Sharyngina, N., Tsitovitch, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Proceedings, CAV 2010: 22nd International Conference on Computer Aided Verification, Edinburg, UK (2010)","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"457_CR43","doi-asserted-by":"crossref","unstructured":"Lefaucheux, E., Ouaknine, J., Purser, D., Worrell, J.: Porous invariants. In: Proceedings, International Conference on Computer Aided Verification, July (2021)","DOI":"10.1007\/978-3-030-81688-9_8"},{"key":"457_CR44","doi-asserted-by":"crossref","unstructured":"Liu, H., Fu, H., Yu, Z., Song, J., Li, G.: Scalable linear invariant generation with Farkas\u2019 lemma. In: Proceedings, ACM Programming Languages, OOPSLA2 Article 2, vol. 6, October (2022)","DOI":"10.1145\/3563295"},{"issue":"1\/2","key":"457_CR45","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1504\/IJCCBS.2014.059596","volume":"5","author":"A Louhichi","year":"2014","unstructured":"Louhichi, A., Ghardallou, W., Bsaies, K., Jilani, L.L., Mraihi, O., Mili, A.: Verifying loops with invariant relations. Int. J. Crit. Comput. Based Syst. 5(1\/2), 78\u2013102 (2014)","journal-title":"Int. J. Crit. Comput. Based Syst."},{"key":"457_CR46","unstructured":"Maclean, E., Ireland, A., Grov, G.: Synthesizing functional invariants in separation logic. In: Proceedings, Workshop on Invariant Generation: WING 2010, Edinburgh, UK (2010)"},{"key":"457_CR47","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Proceedings, TACAS, pp. 413\u2013427 (2008)","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"457_CR48","doi-asserted-by":"publisher","first-page":"989","DOI":"10.1016\/j.scico.2009.09.009","volume":"74","author":"A Mili","year":"2009","unstructured":"Mili, A., Aharon, S., Nadkarni, Ch.: Mathematics for reasoning about loops. Sci. Comput. Program. 74, 989\u20131020 (2009)","journal-title":"Sci. Comput. Program."},{"key":"457_CR49","doi-asserted-by":"publisher","first-page":"1114","DOI":"10.1016\/j.jsc.2008.11.007","volume":"45","author":"A Mili","year":"2009","unstructured":"Mili, A., Aharon, S., Nadkarni, C., Mraihi, O., Louhichi, A., Jilani, L.L.: Reflexive transitive invariant relations: a basis for computing loop functions. J. Symb. Comput. 45, 1114\u20131143 (2009)","journal-title":"J. Symb. Comput."},{"key":"457_CR50","unstructured":"Mraihi, O.: Calcul automatique des fonctions de boucles: Analyse des relations invariantes. Technical report, Institut Superieur de Gestion, Bardo, Tunisie (2014)"},{"issue":"9","key":"457_CR51","doi-asserted-by":"publisher","first-page":"1212","DOI":"10.1016\/j.scico.2012.05.006","volume":"78","author":"O Mraihi","year":"2013","unstructured":"Mraihi, O., Louhichi, A., Jilani, L.L., Desharnais, J., Mili, A.: Invariant assertions, invariant relations, and invariant functions. Sci. Comput. Program. 78(9), 1212\u20131239 (2013)","journal-title":"Sci. Comput. Program."},{"key":"457_CR52","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.entcs.2009.05.052","volume":"240","author":"MO Myreen","year":"2008","unstructured":"Myreen, M.O., Gordon, M.J.C.: Transforming programs into recursive functions. Electron. Notes Theor. Comput. Sci. 240, 185\u2013200 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"457_CR53","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants and transition predicate abstraction for program termination. In: TACAS, pp. 3\u201310 (2011)","DOI":"10.1007\/978-3-642-19835-9_2"},{"key":"457_CR54","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non linear loop invariant generation using Groebner bases. In: Proceedings, ACM SIGPLAN Principles of Programming Languages, POPL 2004, pp. 381\u2013329 (2004)","DOI":"10.1145\/964001.964028"},{"key":"457_CR55","volume-title":"Relational Mathematics. Encyclopedia of Mathematics and its Applications","author":"G Schmidt","year":"2010","unstructured":"Schmidt, G.: Relational Mathematics. Encyclopedia of Mathematics and its Applications, vol. 132. Cambridge University Press, Cambridge (2010)"},{"key":"457_CR56","volume-title":"Relations and Graphs, Discrete Mathematics for Computer Scientists. EATCS-Monographs on Theoretical Computer Science","author":"G Schmidt","year":"1993","unstructured":"Schmidt, G., Stroehlein, T.: Relations and Graphs, Discrete Mathematics for Computer Scientists. EATCS-Monographs on Theoretical Computer Science. Springer, Berlin (1993)"},{"key":"457_CR57","unstructured":"Zuleger, F., Sinn, M.: Loopus: a tool for computing loop bounds for C programs. In: Proceedings, Workshop on Invariant Generation: WING 2010, Edinburgh, UK, July (2010)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-024-00457-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-024-00457-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-024-00457-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T20:26:09Z","timestamp":1731961569000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-024-00457-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,13]]},"references-count":57,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,9]]}},"alternative-id":["457"],"URL":"https:\/\/doi.org\/10.1007\/s00236-024-00457-9","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,5,13]]},"assertion":[{"value":"16 July 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 May 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}