{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:46Z","timestamp":1780994626381,"version":"3.54.1"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816841","type":"print"},{"value":"9783030816858","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper is a tutorial on algebraic program analysis. It explains the foundations of algebraic program analysis, its strengths and limitations, and gives examples of algebraic program analyses for numerical invariant generation and termination analysis.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_3","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"46-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Algebraic Program Analysis"],"prefix":"10.1007","author":[{"given":"Zachary","family":"Kincaid","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Cyphert","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"3_CR1","volume-title":"The Design and Analysis of Computer Algorithms","author":"AV Aho","year":"1974","unstructured":"Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms, 1st edn. Addison-Wesley Longman Publishing Co., Inc., Boston (1974)","edition":"1"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-40885-4_3","volume-title":"Frontiers of Combining Systems","author":"F Alberti","year":"2013","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Definability of accelerated relations in a theory of arrays and its applications. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 23\u201339. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_3"},{"issue":"3","key":"3_CR3","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/360018.360025","volume":"19","author":"FE Allen","year":"1976","unstructured":"Allen, F.E., Cocke, J.: A program data flow analysis procedure. Commun. ACM 19(3), 137 (1976)","journal-title":"Commun. ACM"},{"issue":"1","key":"3_CR4","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. Electr. Notes Theor. Comp. Sci. 267(1), 3\u201316 (2010)","journal-title":"Electr. Notes Theor. Comp. Sci."},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1093\/imamat\/15.2.161","volume":"15","author":"R Backhouse","year":"1975","unstructured":"Backhouse, R., Carr\u00e9, B.: Regular algebra applied to path-finding problems. J. Inst. Math. Appl. 15, 161\u2013186 (1975)","journal-title":"J. Inst. Math. Appl."},{"issue":"2","key":"3_CR6","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1093\/imamat\/15.2.161","volume":"15","author":"RC Backhouse","year":"1975","unstructured":"Backhouse, R.C., Carr\u00e9, B.A.: Regular algebra applied to path-finding problems. IMA J. Appl. Math. 15(2), 161\u2013186 (1975)","journal-title":"IMA J. Appl. Math."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.: Variance analyses from invariance analyses. In: POPL, pp. 211\u2013224 (2007)","DOI":"10.1145\/1190215.1190249"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-33125-1_16","volume-title":"Static Analysis","author":"S Biallas","year":"2012","unstructured":"Biallas, S., Brauer, J., King, A., Kowalewski, S.: Loop leaping with closures. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 214\u2013230. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33125-1_16"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-17511-4_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Blanc","year":"2010","unstructured":"Blanc, R., Henzinger, T.A., Hottelier, T., Kov\u00e1cs, L.: ABC: algebraic bound computation for loops. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 103\u2013118. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_7"},{"issue":"1","key":"3_CR11","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1016\/S0304-3975(03)00314-1","volume":"309","author":"B Boigelot","year":"2003","unstructured":"Boigelot, B.: On iterating linear transformations over recognizable sets of integers. Theor. Comput. Sci. 309(1), 413\u2013468 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"Computer Aided Verification","author":"B Boigelot","year":"1994","unstructured":"Boigelot, B., Wolper, P.: Symbolic verification with periodic sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 55\u201367. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_43"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-642-00768-2_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Bozga","year":"2009","unstructured":"Bozga, M., G\u00eerlea, C., Iosif, R.: Iterating octagons. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 337\u2013351. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_29"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-14295-6_23","volume-title":"Computer Aided Verification","author":"M Bozga","year":"2010","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227\u2013242. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_23"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1007\/11787006_49","volume-title":"Automata, Languages and Programming","author":"M Bozga","year":"2006","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 577\u2013588. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11787006_49"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Breck, J., Cyphert, J., Kincaid, Z., Reps, T.: Templates and recurrences: better together. In: PLDI, pp. 688\u2013702 (2020)","DOI":"10.1145\/3395656"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Brzozowski, J.A.: Regular-like expressions for some irregular languages. In: SWAT (FOCS), pp. 278\u2013286 (1968)","DOI":"10.1109\/SWAT.1968.24"},{"issue":"6","key":"3_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 1\u201366 (2011)","journal-title":"J. ACM"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-78800-3_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Caniart","year":"2008","unstructured":"Caniart, N., Fleury, E., Leroux, J., Zeitoun, M.: Accelerating interpolation-based model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 428\u2013442. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_32"},{"issue":"1","key":"3_CR20","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.1145\/3121136","volume":"40","author":"H Chen","year":"2018","unstructured":"Chen, H., David, C., Kroening, D., Schrammel, P., Wachter, B.: Bit-precise procedure-modular termination analysis. TOPLAS 40(1), 1:1-1:38 (2018)","journal-title":"TOPLAS"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 268\u2013279. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028751"},{"key":"3_CR22","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: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"3_CR23","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E. (ed.) Formal Descriptions of Programming Concepts, (IFIP WG 2.2, St. Andrews, Canada, August 1977), pp. 237\u2013277. North-Holland (1978)"},{"issue":"4","key":"3_CR24","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput. 2(4), 511\u2013547 (1992)","journal-title":"J. Log. Comput."},{"key":"3_CR25","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3290358"},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/1857914.1857917","volume":"57","author":"J Esparza","year":"2010","unstructured":"Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. J. ACM 57, 6 (2010)","journal-title":"J. ACM"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD, pp. 57\u201364 (2015)","DOI":"10.1109\/FMCAD.2015.7542253"},{"issue":"2","key":"3_CR28","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2010.09.014","volume":"267","author":"P Feautrier","year":"2010","unstructured":"Feautrier, P., Gonnord, L.: Accelerated invariant generation for C programs with aspic and c2fsm. Electr. Notes Theor. Comput. Sci. 267(2), 3\u201313 (2010)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-36206-1_14","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"A Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to compose Presburger-accelerations: applications to broadcast protocols. In: Agrawal, M., Seth, A. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145\u2013156. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36206-1_14"},{"key":"3_CR30","series-title":"Operations Research\/Computer Science Interfaces","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-75450-5","volume-title":"Graphs, Dioids and Semirings: New Models and Algorithms","author":"M Gondran","year":"2008","unstructured":"Gondran, M., Minoux, M.: Graphs, Dioids and Semirings: New Models and Algorithms. ORCS, vol. 41, 1st edn. Springer, Boston (2008). https:\/\/doi.org\/10.1007\/978-0-387-75450-5","edition":"1"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/11823230_10","volume-title":"Static Analysis","author":"L Gonnord","year":"2006","unstructured":"Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 144\u2013160. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11823230_10"},{"issue":"6","key":"3_CR32","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1145\/2813885.2737976","volume":"50","author":"L Gonnord","year":"2015","unstructured":"Gonnord, L., Monniaux, D., Radanne, G.: Synthesis of ranking functions using extremal counterexamples. SIGPLAN Not. 50(6), 608\u2013618 (2015)","journal-title":"SIGPLAN Not."},{"issue":"1","key":"3_CR33","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/321921.321939","volume":"23","author":"SL Graham","year":"1976","unstructured":"Graham, S.L., Wegman, M.N.: A fast and usually linear algorithm for global flow analysis. J. ACM 23(1), 172\u2013202 (1976)","journal-title":"J. ACM"},{"issue":"2","key":"3_CR34","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1016\/S0019-9958(69)90055-2","volume":"14","author":"J Gruska","year":"1969","unstructured":"Gruska, J.: Some classifications of context-free languages. Inf. Control 14(2), 152\u2013179 (1969)","journal-title":"Inf. Control"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-11439-2_9","volume-title":"Reachability Problems","author":"C Haase","year":"2014","unstructured":"Haase, C., Halfon, S.: Integer vector addition systems with states. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 112\u2013124. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_9"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Hecht, M.S., Ullman, J.D.: Analysis of a simple algorithm for global data flow problems. In: POPL, pp. 207\u2013217 (1973)","DOI":"10.1145\/512927.512946"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-33386-6_16","volume-title":"Automated Technology for Verification and Analysis","author":"H Hojjat","year":"2012","unstructured":"Hojjat, H., Iosif, R., Kone\u010dn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 187\u2013202. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_16"},{"key":"3_CR38","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M Karr","year":"1976","unstructured":"Karr, M.: Affine relationship among variables of a program. Acta Inf. 6, 133\u2013151 (1976)","journal-title":"Acta Inf."},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Kildall, G.: A unified approach to global program optimization. In: POPL (1973)","DOI":"10.1145\/512927.512945"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional recurrence analysis revisited. In: PLDI, pp. 248\u2013262 (2017)","DOI":"10.1145\/3140587.3062373"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Breck, J., Cyphert, J., Reps, T.W.: Closed forms for numerical loops. Proc. ACM Program. Lang. 3(POPL), 55:1\u201355:29 (2019)","DOI":"10.1145\/3290368"},{"key":"3_CR42","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3158142"},{"issue":"7","key":"3_CR43","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"3_CR44","first-page":"3","volume-title":"Automata Stud.","author":"S Kleene","year":"1956","unstructured":"Kleene, S.: Representation of events in nerve nets and finite automata. In: Shannon, C., McCarthy, J. (eds.) Automata Stud., pp. 3\u201340. Princeton University Press, Princeton (1956)"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-662-49674-9_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Kone\u010dn\u00fd","year":"2016","unstructured":"Kone\u010dn\u00fd, F.: PTIME computation of transitive closures of octagonal relations. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 645\u2013661. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_42"},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-39799-8_26","volume-title":"Computer Aided Verification","author":"D Kroening","year":"2013","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 381\u2013396. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_26"},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-88387-6_10","volume-title":"Automated Technology for Verification and Analysis","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 111\u2013125. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88387-6_10"},{"issue":"1","key":"3_CR48","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/0304-3975(77)90056-1","volume":"4","author":"DJ Lehmann","year":"1977","unstructured":"Lehmann, D.J.: Algebraic structures for transitive closure. Theoret. Comput. Sci. 4(1), 59\u201376 (1977)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"3_CR49","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1109\/TEC.1960.5221603","volume":"9","author":"R McNaughton","year":"1960","unstructured":"McNaughton, R., Yamada, H.: Regular expressions and state graphs for automata. IRE Trans. Electron. Comput. 9(1), 39\u201347 (1960)","journal-title":"IRE Trans. Electron. Comput."},{"issue":"3","key":"3_CR50","first-page":"321","volume":"7","author":"M Mohri","year":"2002","unstructured":"Mohri, M.: Semiring frameworks and algorithms for shortest-distance problems. J. Autom. Lang. Comb. 7(3), 321\u2013350 (2002)","journal-title":"J. Autom. Lang. Comb."},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Automatic modular abstractions for linear constraints. In: POPL, pp. 140\u2013151 (2009)","DOI":"10.1145\/1594834.1480899"},{"issue":"1\u20132","key":"3_CR52","first-page":"206","volume":"58","author":"T Reps","year":"2005","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. SCP 58(1\u20132), 206\u2013263 (2005)","journal-title":"SCP"},{"key":"3_CR53","doi-asserted-by":"crossref","unstructured":"Reps, T., Turetsky, E., Prabhu, P.: Newtonian program analysis via tensor product. TOPLAS 39(2), 9:1\u20139:72 (2017)","DOI":"10.1145\/3024084"},{"issue":"3","key":"3_CR54","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1145\/27632.27649","volume":"18","author":"BG Ryder","year":"1986","unstructured":"Ryder, B.G., Paull, M.C.: Elimination algorithms for data flow analysis. ACM Comput. Surv. (CSUR) 18(3), 277\u2013316 (1986)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"3_CR55","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-642-31365-3_38","volume-title":"Automated Reasoning","author":"R Sebastiani","year":"2012","unstructured":"Sebastiani, R., Tomasi, S.: Optimization in SMT with $${\\cal{L}A}$$($$\\mathbb{Q}$$) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 484\u2013498. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_38"},{"key":"3_CR56","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications. Prentice-Hall (1981)"},{"key":"3_CR57","unstructured":"Szab\u00f3, Z.: Compositionality (2020). https:\/\/plato.stanford.edu\/entries\/compositionality\/"},{"issue":"3","key":"3_CR58","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1145\/322261.322273","volume":"28","author":"RE Tarjan","year":"1981","unstructured":"Tarjan, R.E.: Fast algorithms for solving path problems. J. ACM 28(3), 594\u2013614 (1981)","journal-title":"J. ACM"},{"issue":"3","key":"3_CR59","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1145\/322261.322272","volume":"28","author":"RE Tarjan","year":"1981","unstructured":"Tarjan, R.E.: A unified approach to path problems. J. ACM 28(3), 577\u2013593 (1981)","journal-title":"J. ACM"},{"key":"3_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-19835-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Tsitovich","year":"2011","unstructured":"Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 81\u201395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_9"},{"key":"3_CR61","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1016\/S0019-9958(67)91032-7","volume":"10","author":"M Yntema","year":"1967","unstructured":"Yntema, M.: Inclusion relations among families of context-free languages. Inf. Control 10, 572\u2013597 (1967)","journal-title":"Inf. Control"},{"key":"3_CR62","doi-asserted-by":"crossref","unstructured":"Zhu, S., Kincaid, Z.: Reflections on termination of linear loops. In: CAV (2021)","DOI":"10.1007\/978-3-030-81688-9_3"},{"key":"3_CR63","doi-asserted-by":"crossref","unstructured":"Zhu, S., Kincaid, Z.: Termination analysis without the tears. In: PLDI (2021)","DOI":"10.1145\/3453483.3454110"},{"key":"3_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-23702-7_22","volume-title":"Static Analysis","author":"F Zuleger","year":"2011","unstructured":"Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280\u2013297. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_22"}],"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-030-81685-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:04:22Z","timestamp":1626480262000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}