{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T18:05:01Z","timestamp":1746295501964,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030816872"},{"type":"electronic","value":"9783030816889"}],"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>We introduce the notion of <jats:italic>porous invariants<\/jats:italic> for multipath (or branching\/nondeterministic) affine loops over the integers; these invariants are not necessarily convex, and can in fact contain infinitely many \u2018holes\u2019. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle (non-)reachability questions for various interesting classes of affine loops and target sets.\n<\/jats:p>","DOI":"10.1007\/978-3-030-81688-9_8","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:20:47Z","timestamp":1626452447000},"page":"172-194","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Porous Invariants"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0875-300X","authenticated-orcid":false,"given":"Engel","family":"Lefaucheux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0031-9356","authenticated-orcid":false,"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0394-1634","authenticated-orcid":false,"given":"David","family":"Purser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8151-2443","authenticated-orcid":false,"given":"James","family":"Worrell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"8_CR1","unstructured":"Almagor, S., Chistikov, D., Ouaknine, J., Worrell, J.: O-minimal invariants for discrete-time dynamical systems (2019, preprint, submitted). https:\/\/arxiv.org\/abs\/1802.09263"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Bozga, M., Iosif, R., Konecn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P.B. (eds.) Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, 15\u201319 July 2010. Proceedings. Lecture Notes in Computer Science, vol. 6174, pp. 227\u2013242. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_23. Extended VERIMAG technical report, TR-2012-10, 2012: http:\/\/www-verimag.imag.fr\/TR\/TR-2012-10.pdf","DOI":"10.1007\/978-3-642-14295-6_23"},{"issue":"4","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1838","DOI":"10.1007\/BF01095643","volume":"34","author":"A Chistov","year":"1986","unstructured":"Chistov, A.: Algorithm of polynomial complexity for factoring polynomials and finding the components of varieties in subexponential time. J. Soviet Math. 34(4), 1838\u20131882 (1986). https:\/\/doi.org\/10.1007\/BF01095643","journal-title":"J. Soviet Math."},{"issue":"4","key":"8_CR4","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., et al.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583\u2013604 (2003). https:\/\/doi.org\/10.1142\/S012905410300190X","journal-title":"Int. J. Found. Comput. Sci."},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 84\u201396. ACM Press (1978). https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"issue":"3","key":"8_CR6","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1051\/ita\/2012015","volume":"46","author":"J Dong","year":"2012","unstructured":"Dong, J., Liu, Q.: Undecidability of infinite post correspondence problem for instances of size 8. RAIRO Theor. Informatics Appl. 46(3), 451\u2013457 (2012). https:\/\/doi.org\/10.1051\/ita\/2012015","journal-title":"RAIRO Theor. Informatics Appl."},{"key":"8_CR7","volume-title":"G\u00f6del, Escher, Bach: An Eternal Golden Braid","author":"RH Douglas","year":"1979","unstructured":"Douglas, R.H.: G\u00f6del, Escher, Bach: An Eternal Golden Braid. Basic Books, New York (1979)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-030-32304-2_9","volume-title":"Static Analysis","author":"N Fijalkow","year":"2019","unstructured":"Fijalkow, N., Lefaucheux, E., Ohlmann, P., Ouaknine, J., Pouly, A., Worrell, J.: On the Monniaux problem in abstract interpretation. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 162\u2013180. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_9"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-3-642-40313-2_37","volume-title":"Mathematical Foundations of Computer Science 2013","author":"A Finkel","year":"2013","unstructured":"Finkel, A., G\u00f6ller, S., Haase, C.: Reachability in register machines with polynomial updates. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 409\u2013420. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40313-2_37"},{"key":"8_CR10","unstructured":"Fremont, D.: The reachability problem for affine functions on the integers. CoRR abs\/1304.2639 (2013). http:\/\/arxiv.org\/abs\/1304.2639"},{"issue":"1","key":"8_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2016","unstructured":"Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58(1), 3\u201331 (2016). https:\/\/doi.org\/10.1007\/s10817-016-9388-y","journal-title":"J. Autom. Reason."},{"issue":"2","key":"8_CR12","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1090\/S0002-9947-1964-0181500-1","volume":"113","author":"S Ginsburg","year":"1964","unstructured":"Ginsburg, S., Spanier, E.H.: Bounded ALGOL-like languages. Trans. Am. Math. Soc. 113(2), 333\u2013368 (1964). https:\/\/doi.org\/10.1090\/S0002-9947-1964-0181500-1","journal-title":"Trans. Am. Math. Soc."},{"issue":"4","key":"8_CR13","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1051\/ita:2006039","volume":"40","author":"V Halava","year":"2006","unstructured":"Halava, V., Harju, T.: Undecidability of infinite post correspondence problem for instances of size 9. RAIRO Theor. Informatics Appl. 40(4), 551\u2013557 (2006). https:\/\/doi.org\/10.1051\/ita:2006039","journal-title":"RAIRO Theor. Informatics Appl."},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1007\/978-3-319-08867-9_53","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2014","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 797\u2013813. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_53"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: Polynomial invariants for affine programs. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, 09\u201312 July 2018, pp. 530\u2013539. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209142","DOI":"10.1145\/3209108.3209142"},{"issue":"4","key":"8_CR16","doi-asserted-by":"publisher","first-page":"808","DOI":"10.1145\/6490.6496","volume":"33","author":"R Kannan","year":"1986","unstructured":"Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM 33(4), 808\u2013821 (1986). https:\/\/doi.org\/10.1145\/6490.6496","journal-title":"J. ACM"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133\u2013151 (1976). https:\/\/doi.org\/10.1007\/BF00268497","DOI":"10.1007\/BF00268497"},{"key":"8_CR18","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3290368","DOI":"10.1145\/3290368"},{"issue":"53","key":"8_CR19","first-page":"173","volume":"57","author":"L Kronecker","year":"1857","unstructured":"Kronecker, L.: Zwei S\u00e4tze \u00fcber Gleichungen mit ganzzahligen Coefficienten. Journal f\u00fcr die reine und angewandte Mathematik 57(53), 173\u2013175 (1857)","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Leroux, J.: The general vector addition system reachability problem by presburger inductive invariants. Log. Methods Comput. Sci. 6(3) (2010). https:\/\/doi.org\/10.2168\/LMCS-6(3:22)2010","DOI":"10.2168\/LMCS-6(3:22)2010"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Leroux, J.: Vector addition system reachability problem: a short self-contained proof. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 January 2011, pp. 307\u2013316. ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926421","DOI":"10.1145\/1926385.1926421"},{"key":"8_CR22","first-page":"539","volume":"57","author":"A Markov","year":"1947","unstructured":"Markov, A.: On certain insoluble problems concerning matrices. Doklady Akad. Nauk SSSR. 57, 539\u2013542 (1947)","journal-title":"Doklady Akad. Nauk SSSR."},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: On the decidability of the existence of polyhedral invariants in transition systems. Acta Informatica 56(4), 385\u2013389 (2018). https:\/\/doi.org\/10.1007\/s00236-018-0324-y","DOI":"10.1007\/s00236-018-0324-y"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-33512-9_3","volume-title":"Reachability Problems","author":"J Ouaknine","year":"2012","unstructured":"Ouaknine, J., Worrell, J.: Decision problems for linear recurrence sequences. In: Finkel, A., Leroux, J., Potapov, I. (eds.) RP 2012. LNCS, vol. 7550, pp. 21\u201328. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33512-9_3"},{"key":"8_CR25","unstructured":"Shmonin, G.: Lattices and Hermite normal form, February 2009. Lecture notes for the course Integer Points in Polyhedra at the Swiss Federal Institute of Technology Lausanne (EPFL)"},{"issue":"2","key":"8_CR26","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1137\/0221017","volume":"21","author":"W Tzeng","year":"1992","unstructured":"Tzeng, W.: A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM J. Comput. 21(2), 216\u2013227 (1992). https:\/\/doi.org\/10.1137\/0221017","journal-title":"SIAM J. Comput."}],"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-81688-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:22:04Z","timestamp":1626452524000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81688-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816872","9783030816889"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81688-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"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)"}}]}}