{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T22:00:37Z","timestamp":1775340037037,"version":"3.50.1"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031223075","type":"print"},{"value":"9783031223082","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-22308-2_3","type":"book-chapter","created":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T19:55:03Z","timestamp":1669924503000},"page":"19-43","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Solving Invariant Generation for\u00a0Unsolvable Loops"],"prefix":"10.1007","author":[{"given":"Daneshvar","family":"Amrollahi","sequence":"first","affiliation":[]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[]},{"given":"George","family":"Kenison","sequence":"additional","affiliation":[]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]},{"given":"Marcel","family":"Moosbrugger","sequence":"additional","affiliation":[]},{"given":"Miroslav","family":"Stankovi\u010d","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,2]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovic, M.: Automatic generation of moment-based invariants for Prob-solvable loops. In: Proceedings of ATVA, pp. 255\u2013276 (2019)","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovic, M.: Analysis of Bayesian networks via Prob-solvable loops. In: Proceedings of ICTAC, pp. 221\u2013241 (2020)","DOI":"10.1007\/978-3-030-64276-1_12"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Britton, N.F., Franks, N.R., Pratt, S.C., Seeley, T.D.: Deciding on a new home: how do honeybees agree? Proceedings of the Royal Society of London. Series B: Biological Sciences, vol. 269(1498), pp. 1383\u20131388 (2002)","DOI":"10.1098\/rspb.2002.2001"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification, pp. 511\u2013526. Springer, Berlin Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Voronin, Y.L., Sankaranarayanan, S.: Deductive proofs of almost sure persistence and recurrence properties. In: Proceedings of TACAS, pp. 260\u2013279 (2016)","DOI":"10.1007\/978-3-662-49674-9_15"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Dreossi, T., Dang, T., Piazza, C.: Parallelotope bundles for polynomial reachability. In: Proceedings of HSCC, pp. 297\u2013306 (2016)","DOI":"10.1145\/2883817.2883838"},{"key":"3_CR7","unstructured":"Elspas, B., Green, M., Levitt, K., Waldinger, R.: Research in Interactive Program-Proving Techniques. Technical report, SRI (1972)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Everest, G., van der Poorten, A., Shparlinski, I., Ward, T.: Recurrence Sequences, Math. Surveys Monogr., vol. 104. Amer. Math. Soc., Providence, RI (2003)","DOI":"10.1090\/surv\/104"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD, pp. 57\u201364 (2015)","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Frohn, F., Hark, M., Giesl, J.: Termination of polynomial loops. In: Proceedings of SAS, pp. 89\u2013112 (2020)","DOI":"10.1007\/978-3-030-65474-0_5"},{"issue":"10","key":"3_CR11","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: Polynomial invariants for affine programs. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2018). Association for Computing Machinery, New York, NY, USA, pp. 530\u2013539 (2018). https:\/\/doi.org\/10.1145\/3209108.3209142","DOI":"10.1145\/3209108.3209142"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Huang, Z., Fan, C., Mereacre, A., Mitra, S., Kwiatkowska, M.Z.: Invariant verification of nonlinear hybrid automata networks of cardiac cells. In: Proceedings of CAV, pp. 373\u2013390 (2014)","DOI":"10.1007\/978-3-319-08867-9_25"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Aligator.jl - A Julia package for loop invariant generation. In: Proceedings of CICM, pp. 111\u2013117 (2018)","DOI":"10.1007\/978-3-319-96812-4_10"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Automated generation of non-linear loop invariants utilizing hypergeometric sequences. In: Proceedings of ISSAC, pp. 221\u2013228 (2017)","DOI":"10.1145\/3087604.3087623"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Invariant generation for multi-path loops with polynomial assignments. In: Proceedings of VMCAI, pp. 226\u2013246 (2018)","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: Proceedings of ESOP, pp. 364\u2013389 (2016)","DOI":"10.1007\/978-3-662-49498-1_15"},{"issue":"4","key":"3_CR18","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1145\/360032.360048","volume":"19","author":"S Katz","year":"1976","unstructured":"Katz, S., Manna, Z.: Logical analysis of programs. Commun. ACM 19(4), 188\u2013206 (1976)","journal-title":"Commun. ACM"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Kauers, M., Paule, P.: The Concrete Tetrahedron. Texts and Monographs in Symbolic Computation. Springer Vienna (2011). https:\/\/doi.org\/10.1007\/978-3-211-99314-9","DOI":"10.1007\/978-3-211-99314-9"},{"key":"3_CR20","doi-asserted-by":"publisher","first-page":"787","DOI":"10.1016\/j.jsc.2008.03.002","volume":"43","author":"M Kauers","year":"2008","unstructured":"Kauers, M., Zimmermann, B.: Computing the algebraic relations of C-finite sequences and Multisequences. J. Symb. Comput. 43, 787\u2013803 (2008)","journal-title":"J. Symb. Comput."},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. In: Proceedings of POPL, pp. 54:1\u201354:33 (2018)","DOI":"10.1145\/3158142"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L.: Reasoning algebraically about P-solvable loops. In: Proceedings of TACAS, pp. 249\u2013264 (2008)","DOI":"10.1007\/978-3-540-78800-3_18"},{"key":"3_CR23","unstructured":"Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proceedings of CGO, pp. 75\u201388 (2004)"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Meurer, A., et al.: SymPy: symbolic computing in Python. Peer J. Comput. Sci. 3, e103 (2017)","DOI":"10.7717\/peerj-cs.103"},{"key":"3_CR25","unstructured":"Moosbrugger, M., Stankovic, M., Bartocci, E., Kov\u00e1cs, L.: This is the moment for probabilistic loops. CoRR abs\/2204.07185 (2022). To appear in the proceedings of OOPSLA 2022"},{"issue":"5","key":"3_CR26","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","volume":"91","author":"M M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett. 91(5), 233\u2013244 (2004)","journal-title":"Inf. Process. Lett."},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: Proceedings of ATVA, pp. 479\u2013494 (2016)","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. 443\u2013476 (2007)","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: Proceedings of ISSAC, p. 266\u2013273 (2004)","DOI":"10.1145\/1005285.1005324"},{"key":"3_CR30","unstructured":"Sankaranarayanan, S., Chou, Y., Goubault, E., Putot, S.: Reasoning about uncertainties in discrete-time dynamical systems using polynomial forms. In: Proceedings of NeurIPS, pp. 17502\u201317513 (2020)"},{"key":"3_CR31","unstructured":"Schreuder, A., Ong, C.L.: Polynomial Probabilistic Invariants and the Optional Stopping Theorem. CoRR abs\/1910.12634 (2019)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22308-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T19:55:40Z","timestamp":1669924540000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22308-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223075","9783031223082"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22308-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"2 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Auckland","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Zealand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 December 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.staticanalysis.org\/","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":"43","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":"18","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":"42% - 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.2","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":"6.1","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)"}}]}}