{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T02:21:16Z","timestamp":1785291676105,"version":"3.55.0"},"publisher-location":"Cham","reference-count":89,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031826993","type":"print"},{"value":"9783031827006","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-82700-6_9","type":"book-chapter","created":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T01:26:26Z","timestamp":1737595586000},"page":"187-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Affine Disjunctive Invariant Generation with\u00a0Farkas\u2019 Lemma"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-6848-3105","authenticated-orcid":false,"given":"Jingyu","family":"Ke","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7947-3446","authenticated-orcid":false,"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8987-596X","authenticated-orcid":false,"given":"Hongming","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-8863-5548","authenticated-orcid":false,"given":"Zhouyue","family":"Sun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8084-8009","authenticated-orcid":false,"given":"Liqian","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-7112","authenticated-orcid":false,"given":"Guoqiang","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,1,24]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-662-48288-9_14","volume-title":"Static Analysis","author":"A Adj\u00e9","year":"2015","unstructured":"Adj\u00e9, A., Garoche, P.-L., Magron, V.: Property-based polynomial invariant generation using sums-of-squares optimization. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 235\u2013251. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_14"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-31424-7_48","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672\u2013678. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_48"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-15769-1_8","volume-title":"Static Analysis","author":"C Alias","year":"2010","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117\u2013133. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_8"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A.K., Mahdavi, M.: Polynomial reachability witnesses via stellens\u00e4tze. In: PLDI, pp. 772\u2013787. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454076","DOI":"10.1145\/3453483.3454076"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-44898-5_19","volume-title":"Static Analysis","author":"R Bagnara","year":"2003","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 337\u2013354. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_19"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45789-5_17","volume-title":"Static Analysis","author":"R Bagnara","year":"2002","unstructured":"Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213\u2013229. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45789-5_17"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Balakrishnan, G., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Refining the control structure of loops using static analysis. In: Chakraborty, S., Halbwachs, N. (eds.) Proceedings of the 9th ACM & IEEE International conference on Embedded software, EMSOFT 2009, Grenoble, France, 12\u201316 October 2009, pp. 49\u201358. ACM (2009). https:\/\/doi.org\/10.1145\/1629335.1629343","DOI":"10.1145\/1629335.1629343"},{"key":"9_CR8","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104620","volume":"275","author":"A Becchi","year":"2020","unstructured":"Becchi, A., Zaffanella, E.: Pplite: zero-overhead encoding of nnc polyhedra. Inf. Comput. 275, 104620 (2020)","journal-title":"Inf. Comput."},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-030-11245-5_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Boutonnet","year":"2019","unstructured":"Boutonnet, R., Halbwachs, N.: Disjunctive relational abstract interpretation for interprocedural program analysis. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 136\u2013159. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_7"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491\u2013504. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_48"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-319-10431-7_20","volume-title":"Software Engineering and Formal Methods","author":"G Brat","year":"2014","unstructured":"Brat, G., Navas, J.A., Shi, N., Venet, A.: IKOS: a framework for static analysis based on abstract interpretation. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 271\u2013277. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_20"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26:1\u201326:66 (2011). https:\/\/doi.org\/10.1145\/2049697.2049700","DOI":"10.1145\/2049697.2049700"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Non-polynomial worst-case analysis of recursive programs. ACM Trans. Program. Lang. Syst. 41(4), 20:1\u201320:52 (2019). https:\/\/doi.org\/10.1145\/3339984","DOI":"10.1145\/3339984"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K., Goharshady, E.K.: Polynomial invariant generation for non-deterministic recursive programs. In: PLDI, pp. 672\u2013687. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385969","DOI":"10.1145\/3385412.3385969"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-75292-9_3","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2007","author":"Y Chen","year":"2007","unstructured":"Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering non-linear ranking functions by solving semi-algebraic systems. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 34\u201349. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75292-9_3"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1007\/978-3-319-21690-4_44","volume-title":"Computer Aided Verification","author":"Y-F Chen","year":"2015","unstructured":"Chen, Y.-F., Hong, C.-D., Wang, B.-Y., Zhang, L.: Counterexample-guided polynomial loop invariant generation by lagrange interpolation. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 658\u2013674. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_44"},{"key":"9_CR18","unstructured":"Clang static analyzer: a source code analysis tool that finds bugs in c, c++, and objective-c programs (2022). https:\/\/clang-analyzer.llvm.org\/"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_39"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MA Col\u00f3on","year":"2001","unstructured":"Col\u00f3on, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67\u201381. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_6"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1\u201324. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_1"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The astr\u00e9e analyzer. In: Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, 4\u20138 April 2005. Proceedings 14, pp. 21\u201330. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201396. ACM Press (1978). https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"9_CR25","unstructured":"Cpachecker: The configurable software-verification platform (2022). https:\/\/cpachecker.sosy-lab.org"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Csallner, C., Tillmann, N., Smaragdakis, Y.: Dysy: dynamic symbolic execution for invariant inference. In: ICSE, pp. 281\u2013290. ACM (2008).https:\/\/doi.org\/10.1145\/1368088.1368127","DOI":"10.1145\/1368088.1368127"},{"key":"9_CR27","doi-asserted-by":"publisher","unstructured":"Cyphert, J., Breck, J., Kincaid, Z., Reps, T.W.: Refinement of path expressions for static analysis. Proc. ACM Program. Lang. 3(POPL), 45:1\u201345:29 (2019). https:\/\/doi.org\/10.1145\/3290358","DOI":"10.1145\/3290358"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Darke, P., Agrawal, S., Venkatesh, R.: Veriabs: a tool for scalable verification by abstraction (competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems: 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, 27 March\u20131 April 2021, Proceedings, Part II 27, pp. 458\u2013462. Springer, Heidelberg (2021)","DOI":"10.1007\/978-3-030-72013-1_32"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-319-48989-6_12","volume-title":"FM 2016: Formal Methods","author":"C David","year":"2016","unstructured":"David, C., Kesseli, P., Kroening, D., Lewis, M.: Danger invariants. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 182\u2013198. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_12"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: OOPSLA, pp. 443\u2013456. ACM (2013). https:\/\/doi.org\/10.1145\/2509136.2509511","DOI":"10.1145\/2509136.2509511"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-23702-7_26","volume-title":"Static Analysis","author":"AF Donaldson","year":"2011","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., R\u00fcmmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 351\u2013368. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_26"},{"key":"9_CR32","first-page":"457","volume":"12","author":"J Farkas","year":"1894","unstructured":"Farkas, J.: A fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6 12, 457\u2013472 (1894)","journal-title":"Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD, pp. 57\u201364. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-53288-8_20","volume-title":"Computer Aided Verification","author":"T Gan","year":"2020","unstructured":"Gan, T., Xia, B., Xue, B., Zhan, N., Dai, L.: Nonlinear craig interpolant generation. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 415\u2013438. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_20"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE:\u00a0a\u00a0robust\u00a0framework\u00a0for\u00a0learning\u00a0invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: POPL, pp. 499\u2013512. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837664","DOI":"10.1145\/2837614.2837664"},{"key":"9_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-74061-2_22","volume-title":"Static Analysis","author":"D Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.: Guided static analysis. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349\u2013365. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_22"},{"key":"9_CR38","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: Hind, M., Diwan, A. (eds.) Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, 15\u201321 June 2009, pp. 375\u2013385. ACM (2009). https:\/\/doi.org\/10.1145\/1542476.1542518","DOI":"10.1145\/1542476.1542518"},{"key":"9_CR39","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281\u2013292. ACM (2008). https:\/\/doi.org\/10.1145\/1375581.1375616","DOI":"10.1145\/1375581.1375616"},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-642-02658-4_48","volume-title":"Computer Aided Verification","author":"A Gupta","year":"2009","unstructured":"Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 634\u2013640. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_48"},{"key":"9_CR41","doi-asserted-by":"publisher","unstructured":"He, J., Singh, G., P\u00fcschel, M., Vechev, M.T.: Learning fast and precise numerical analysis. In: PLDI, pp. 1112\u20131127. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3386016","DOI":"10.1145\/3385412.3386016"},{"key":"9_CR42","doi-asserted-by":"publisher","unstructured":"Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. Electron. Notes Theor. Comput. Sci. 289, 15\u201325 (2012). https:\/\/doi.org\/10.1016\/j.entcs.2012.11.003","DOI":"10.1016\/j.entcs.2012.11.003"},{"key":"9_CR43","doi-asserted-by":"publisher","unstructured":"Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: Polynomial invariants for affine programs. In: LICS, pp. 530\u2013539. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209142","DOI":"10.1145\/3209108.3209142"},{"key":"9_CR44","doi-asserted-by":"publisher","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Automated generation of non-linear loop invariants utilizing hypergeometric sequences. In: ISSAC, pp. 221\u2013228. ACM (2017). https:\/\/doi.org\/10.1145\/3087604.3087623","DOI":"10.1145\/3087604.3087623"},{"key":"9_CR45","doi-asserted-by":"publisher","unstructured":"Ji, Y., Fu, H., Fang, B., Chen, H.: Affine loop invariant generation via matrix algebra. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, 7\u201310 August 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 257\u2013281. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_13","DOI":"10.1007\/978-3-031-13185-1_13"},{"key":"9_CR46","doi-asserted-by":"publisher","unstructured":"K., H.G.V., Shoham, S., Gurfinkel, A.: Solving constrained horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6(POPL), 1\u201329 (2022). https:\/\/doi.org\/10.1145\/3498722","DOI":"10.1145\/3498722"},{"key":"9_CR47","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Deduction and Applications. Dagstuhl Seminar Proceedings, vol. 05431. Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany (2005). http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/511"},{"key":"9_CR48","unstructured":"Ke, J., Fu, H., Liu, H., Chen, L., Li, G.: Affine disjunctive invariant generation with farkas\u2019 lemma. arXiv preprint arXiv:2307.13318 (2023)"},{"key":"9_CR49","doi-asserted-by":"publisher","unstructured":"Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional recurrence analysis revisited. In: PLDI, pp. 248\u2013262. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062373","DOI":"10.1145\/3062341.3062373"},{"key":"9_CR50","doi-asserted-by":"publisher","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang. 2(POPL), 54:1\u201354:33 (2018). https:\/\/doi.org\/10.1145\/3158142","DOI":"10.1145\/3158142"},{"key":"9_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-35873-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Larraz","year":"2013","unstructured":"Larraz, D., Rodr\u00edguez-Carbonell, E., Rubio, A.: SMT-based array invariant generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 169\u2013188. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_12"},{"key":"9_CR52","doi-asserted-by":"publisher","unstructured":"Le, T.C., Zheng, G., Nguyen, T.: SLING: using dynamic analysis to infer program invariants in separation logic. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22\u201326 June 2019, pp. 788\u2013801. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314634","DOI":"10.1145\/3314221.3314634"},{"issue":"2","key":"9_CR53","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/s11704-014-3150-6","volume":"8","author":"W Lin","year":"2014","unstructured":"Lin, W., Wu, M., Yang, Z., Zeng, Z.: Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods. Front. Comp. Sci. 8(2), 192\u2013202 (2014). https:\/\/doi.org\/10.1007\/s11704-014-3150-6","journal-title":"Front. Comp. Sci."},{"key":"9_CR54","doi-asserted-by":"publisher","unstructured":"Lin, Y., et al.: Inferring loop invariants for multi-path loops. In: International Symposium on Theoretical Aspects of Software Engineering, TASE 2021, Shanghai, China, 25\u201327 August 2021, pp. 63\u201370. IEEE (2021).https:\/\/doi.org\/10.1109\/TASE52547.2021.00030","DOI":"10.1109\/TASE52547.2021.00030"},{"key":"9_CR55","doi-asserted-by":"publisher","unstructured":"Liu, H., Fu, H., Yu, Z., Song, J., Li, G.: Scalable linear invariant generation with Farkas\u2019 lemma. Proc. ACM Program. Lang. 6(OOPSLA2) (2022). https:\/\/doi.org\/10.1145\/3563295","DOI":"10.1145\/3563295"},{"key":"9_CR56","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer, Heidelberg (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"9_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413\u2013427. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_31"},{"key":"9_CR58","doi-asserted-by":"publisher","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: ICSE, pp. 683\u2013693. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/ICSE.2012.6227149","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"9_CR59","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Nguyen, K., Duong, H.: Syminfer: inferring numerical invariants using symbolic states. In: Proceedings of the ACM\/IEEE 44th International Conference on Software Engineering: Companion Proceedings, pp. 197\u2013201 (2022)","DOI":"10.1145\/3510454.3516833"},{"key":"9_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-46520-3_30","volume-title":"Automated Technology for Verification and Analysis","author":"S de Oliveira","year":"2016","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 479\u2013494. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_30"},{"key":"9_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-319-68167-2_22","volume-title":"Automated Technology for Verification and Analysis","author":"S de Oliveira","year":"2017","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Synthesizing invariants by solving solvable loops. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 327\u2013343. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_22"},{"key":"9_CR62","doi-asserted-by":"publisher","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: PLDI, pp. 614\u2013630. ACM (2016). https:\/\/doi.org\/10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"9_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20"},{"key":"9_CR64","doi-asserted-by":"crossref","unstructured":"Riley, D., Fedyukovich, G.: Multi-phase invariant synthesis. In: Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 607\u2013619 (2022)","DOI":"10.1145\/3540250.3549166"},{"key":"9_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-27864-1_21","volume-title":"Static Analysis","author":"E Rodr\u00edguez-Carbonell","year":"2004","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 280\u2013295. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_21"},{"key":"9_CR66","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: ISSAC, pp. 266\u2013273. ACM (2004). https:\/\/doi.org\/10.1145\/1005285.1005324","DOI":"10.1145\/1005285.1005324"},{"key":"9_CR67","unstructured":"Ryan, G., Wong, J., Yao, J., Gu, R., Jana, S.: CLN2INV: learning loop invariants with continuous logic networks. In: 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, 26\u201330 April 2020. OpenReview.net (2020). https:\/\/openreview.net\/forum?id=HJlfuTEtvB"},{"key":"9_CR68","doi-asserted-by":"publisher","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using gr\u00f6bner bases. In: POPL, pp. 318\u2013329. ACM (2004).https:\/\/doi.org\/10.1145\/964001.964028","DOI":"10.1145\/964001.964028"},{"key":"9_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"Static Analysis","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 53\u201368. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_7"},{"key":"9_CR70","unstructured":"Schrijver, A.: Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization, Wiley (1999)"},{"issue":"3","key":"9_CR71","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s10703-016-0248-5","volume":"48","author":"R Sharma","year":"2016","unstructured":"Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. Formal Methods Syst. Des. 48(3), 235\u2013256 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0248-5","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/978-3-642-22110-1_57","volume-title":"Computer Aided Verification","author":"R Sharma","year":"2011","unstructured":"Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 703\u2013719. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_57"},{"key":"9_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-642-37036-6_31","volume-title":"Programming Languages and Systems","author":"R Sharma","year":"2013","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 574\u2013592. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_31"},{"key":"9_CR74","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., et al.: Civl: the concurrency intermediate verification language. In: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, pp. 1\u201312 (2015)","DOI":"10.1145\/2807591.2807635"},{"key":"9_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-030-25543-5_7","volume-title":"Computer Aided Verification","author":"J Silverman","year":"2019","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 97\u2013115. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_7"},{"key":"9_CR76","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 46\u201359. ACM (2017)","DOI":"10.1145\/3009837.3009885"},{"key":"9_CR77","unstructured":"Somenzi, F., Bradley, A.R.: IC3: where monolithic and incremental meet. In: Bjesse, P., Slobodov\u00e1, A. (eds.) International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911, Austin, TX, USA, 30 October\u201302 November 2011, pp.\u00a03\u20138. FMCAD Inc. (2011). http:\/\/dl.acm.org\/citation.cfm?id=2157657"},{"key":"9_CR78","doi-asserted-by":"publisher","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: Hind, M., Diwan, A. (eds.) Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, 15\u201321 June 2009, pp. 223\u2013234. ACM (2009). https:\/\/doi.org\/10.1145\/1542476.1542501","DOI":"10.1145\/1542476.1542501"},{"key":"9_CR79","unstructured":"Sting: Stanford invariant generator (2006). http:\/\/theory.stanford.edu\/~srirams\/Software\/sting.html"},{"key":"9_CR80","unstructured":"Software verification competition (2023). https:\/\/sv-comp.sosy-lab.org"},{"issue":"2","key":"9_CR81","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"9_CR82","doi-asserted-by":"crossref","unstructured":"Wang, C., Lin, F.: Solving conditional linear recurrences for program verification: the periodic case. In: OOPSLA. ACM (2023)","DOI":"10.1145\/3554354"},{"key":"9_CR83","doi-asserted-by":"publisher","unstructured":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Quantitative analysis of assertion violations in probabilistic programs. In: PLD, pp. 1171\u20131186. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454102","DOI":"10.1145\/3453483.3454102"},{"key":"9_CR84","doi-asserted-by":"publisher","unstructured":"Wen, C., et al.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: International Conference on Computer Aided Verification, pp. 302\u2013328. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_16","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"9_CR85","doi-asserted-by":"publisher","unstructured":"Xie, X., Chen, B., Liu, Y., Le, W., Li, X.: Proteus: computing disjunctive loop summary via path dependency analysis. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, 13\u201318 November 2016, pp. 61\u201372. ACM (2016).https:\/\/doi.org\/10.1145\/2950290.2950340","DOI":"10.1145\/2950290.2950340"},{"key":"9_CR86","doi-asserted-by":"publisher","unstructured":"Xu, R., He, F., Wang, B.: Interval counterexamples for loop invariant learning. In: ESEC\/FSE, pp. 111\u2013122. ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3409752","DOI":"10.1145\/3368089.3409752"},{"key":"9_CR87","doi-asserted-by":"publisher","unstructured":"Yang, L., Zhou, C., Zhan, N., Xia, B.: Recent advances in program verification through computer algebra. Front. Comput. Sci. China 4(1), 1\u201316 (2010). https:\/\/doi.org\/10.1007\/s11704-009-0074-7","DOI":"10.1007\/s11704-009-0074-7"},{"key":"9_CR88","doi-asserted-by":"publisher","unstructured":"Yao, J., Ryan, G., Wong, J., Jana, S., Gu, R.: Learning nonlinear loop invariants with gated continuous logic networks. In: PLDI, pp. 106\u2013120. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385986","DOI":"10.1145\/3385412.3385986"},{"key":"9_CR89","unstructured":"Z3 (2023). https:\/\/github.com\/Z3Prover\/z3"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-82700-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T01:26:50Z","timestamp":1737595610000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-82700-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031826993","9783031827006"],"references-count":89,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-82700-6_9","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":"24 January 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denver, CO","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"20 January 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}