{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:11Z","timestamp":1750309511267,"version":"3.41.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T00:00:00Z","timestamp":1743033600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ERC","award":["AVS-ISS (648701)"],"award-info":[{"award-number":["AVS-ISS (648701)"]}]},{"name":"DFG","award":["389792660"],"award-info":[{"award-number":["389792660"]}]},{"name":"EPSRC Fellowships","award":["EP\/N008197\/1 and EP\/X033813\/1"],"award-info":[{"award-number":["EP\/N008197\/1 and EP\/X033813\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2025,4,30]]},"abstract":"<jats:p>\n            The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: Given a program\n            <jats:italic>P<\/jats:italic>\n            , a safety (e.g., non-reachability) specification\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\varphi\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            , and an abstract domain of invariants\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathcal {D}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            , does there exist an inductive invariant\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathcal {I}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            in\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathcal {D}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            guaranteeing that program\n            <jats:italic>P<\/jats:italic>\n            meets its specification \u03c6? The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers. In this article, we show that the Monniaux Problem is undecidable for unguarded affine programs and semilinear invariants (unions of polyhedra). Moreover, we show that decidability is recovered in the important special case of simple linear loops.\n          <\/jats:p>","DOI":"10.1145\/3704632","type":"journal-article","created":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T03:56:36Z","timestamp":1731988596000},"page":"1-51","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["On the Monniaux Problem in Abstract Interpretation"],"prefix":"10.1145","volume":"72","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6576-4680","authenticated-orcid":false,"given":"Nathanael","family":"Fijalkow","sequence":"first","affiliation":[{"name":"University of Bordeaux, CNRS, LaBRI, Bordeaux, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0875-300X","authenticated-orcid":false,"given":"Engel","family":"Lefaucheux","sequence":"additional","affiliation":[{"name":"Max-Planck-Institute for Software Systems, Saarbrucken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4685-5253","authenticated-orcid":false,"given":"Pierre","family":"Ohlmann","sequence":"additional","affiliation":[{"name":"Institut de Recherche en Informatique Fondamentale, IRIF, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0031-9356","authenticated-orcid":false,"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[{"name":"Max-Planck-Institute for Software Systems, Saarbrucken, Germany and Computer Science, Oxford University, Oxford, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2549-951X","authenticated-orcid":false,"given":"Amaury","family":"Pouly","sequence":"additional","affiliation":[{"name":"Institut de Recherche en Informatique Fondamentale, IRIF, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8151-2443","authenticated-orcid":false,"given":"James","family":"Worrell","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,3,27]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3501299"},{"key":"e_1_3_4_3_2","first-page":"127","volume-title":"Proceedings of the International Symposium on Static Analysis (SAS\u201918) (Lecture Notes in Computer Science, Vol. 11002)","author":"Bakhirkin Alexey","year":"2018","unstructured":"AlexeyBakhirkinand DavidMonniaux. 2018. Extending constraint-only representation of polyhedra with Boolean constraints. In Proceedings of the International Symposium on Static Analysis (SAS\u201918) (Lecture Notes in Computer Science, Vol. 11002), AndreasPodelski(Ed.). Springer, 127\u2013145. DOI:10.1007\/978-3-319-99725-4_10"},{"key":"e_1_3_4_4_2","volume-title":"Computing Jordan Normal Forms Exactly for Commuting Matrices in Polynomial Time","author":"Cai Jin-yi","year":"2000","unstructured":"Jin-yiCai. 2000. Computing Jordan Normal Forms Exactly for Commuting Matrices in Polynomial Time. Technical Report. SUNY at Buffalo."},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794276853"},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0008439500024693"},{"key":"e_1_3_4_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2006.03.009"},{"key":"e_1_3_4_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02945-9"},{"key":"e_1_3_4_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-009-0089-6"},{"key":"e_1_3_4_10_2","volume-title":"Proceedings of the Conference on Principles of Programming Languages (POPL\u201978)","author":"Cousot Patrick","year":"1978","unstructured":"PatrickCousotand NicolasHalbwachs. 1978. Automatic discovery of linear restraints among variables of a program. In Proceedings of the Conference on Principles of Programming Languages (POPL\u201978). ACM Press. DOI:10.1145\/512760.512770"},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.1051\/ITA\/2012015"},{"key":"e_1_3_4_12_2","series-title":"(Mathematical Surveys and Monographs","doi-asserted-by":"crossref","DOI":"10.1090\/surv\/104","volume-title":"Recurrence Sequences","author":"Everest Graham","year":"2003","unstructured":"GrahamEverest, Alf van derPoorten, IgorShparlinski, and ThomasWard. 2003. Recurrence Sequences(Mathematical Surveys and Monographs, Vol. 104). American Mathematical Society, United States."},{"key":"e_1_3_4_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_9"},{"key":"e_1_3_4_14_2","volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS\u201917)","author":"Fijalkow Nathana\u00ebl","year":"2017","unstructured":"Nathana\u00eblFijalkow, PierreOhlmann, Jo\u00eblOuaknine, AmauryPouly, and JamesWorrell. 2017. Semialgebraic invariant synthesis for the Kannan-Lipton orbit problem. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS\u201917). DOI:10.4230\/LIPICS.STACS.2017.29"},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00224-019-09913-3"},{"key":"e_1_3_4_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_6"},{"key":"e_1_3_4_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_16"},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676987"},{"key":"e_1_3_4_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_4_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209142"},{"key":"e_1_3_4_21_2","volume-title":"Proceedings of the Symposium on Theory of Computing (STOC\u201980)","author":"Kannan Ravindran","year":"1980","unstructured":"RavindranKannanand Richard J.Lipton. 1980. The orbit problem is decidable. In Proceedings of the Symposium on Theory of Computing (STOC\u201980). DOI:10.1145\/800141.804673"},{"key":"e_1_3_4_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6496"},{"key":"e_1_3_4_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_4_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_3_4_25_2","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1007\/BF02590997","article-title":"A note on recurring series","volume":"2","author":"Lech Christer","year":"1953","unstructured":"ChristerLech. 1953. A note on recurring series. Arkiv Matem.2(1953), 417\u2013421.","journal-title":"Arkiv Matem."},{"key":"e_1_3_4_26_2","article-title":"Eine arithmetische eigenschaft der Taylor Koeffizienten rationaler funktionen","volume":"38","author":"Mahler Kurt","year":"1935","unstructured":"KurtMahler. 1935. Eine arithmetische eigenschaft der Taylor Koeffizienten rationaler funktionen. Proc. Konink. Nederl. Akad. Wetenschapp.38(1935).","journal-title":"Proc. Konink. Nederl. Akad. Wetenschapp."},{"key":"e_1_3_4_27_2","article-title":"On the Taylor coefficients of rational functions","author":"Mahler Kurt","year":"1956","unstructured":"KurtMahler. 1956. On the Taylor coefficients of rational functions. In Proceedings of the Cambridge Philosophical Society. Cambridge University Press.","journal-title":"Proceedings of the Cambridge Philosophical Society"},{"key":"e_1_3_4_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_3_4_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00236-018-0324-Y"},{"key":"e_1_3_4_30_2","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-981-19-9601-6_6","article-title":"Completeness in static analysis by abstract interpretation, a personal point of view","volume":"238","author":"Monniaux David","year":"2023","unstructured":"DavidMonniaux. 2023. Completeness in static analysis by abstract interpretation, a personal point of view. Chall. Softw. Verif.238(2023), 93\u2013108. Retrieved from https:\/\/hal.science\/hal-03857312v2","journal-title":"Chall. Softw. Verif."},{"key":"e_1_3_4_31_2","volume-title":"Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP\u201904)","author":"M\u00fcller-Olm Markus","year":"2004","unstructured":"MarkusM\u00fcller-Olmand HelmutSeidl. 2004. A note on Karr\u2019s algorithm. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP\u201904). DOI:10.1007\/978-3-540-27836-8_85"},{"key":"e_1_3_4_32_2","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Proceedings of the Conference on Computer Aided Verification (CAV\u201905)","author":"Necula George C.","year":"2005","unstructured":"George C.Neculaand SumitGulwani. 2005. Randomized algorithms for program analysis and verification. In Proceedings of the Conference on Computer Aided Verification (CAV\u201905)(Lecture Notes in Computer Science, Vol. 3576), KoushaEtessamiand Sriram K.Rajamani(Eds.). Springer, 1. DOI:10.1007\/11513988_1"},{"key":"e_1_3_4_33_2","volume-title":"Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP\u201914)","author":"Ouaknine Jo\u00ebl","year":"2014","unstructured":"Jo\u00eblOuaknineand JamesWorrell. 2014. Ultimate positivity is decidable for simple linear recurrence sequences. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP\u201914). DOI:10.1007\/978-3-662-43951-7_28"},{"key":"e_1_3_4_34_2","volume-title":"Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201905)","author":"Sankaranarayanan Sriram","year":"2005","unstructured":"SriramSankaranarayanan, Henny B.Sipma, and ZoharManna. 2005. Scalable analysis of linear systems using mathematical programming. In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201905). DOI:10.1007\/978-3-540-30579-8_2"},{"key":"e_1_3_4_35_2","volume-title":"Comptes Rendus du Congr\u00e8s des Math\u00e9maticiens Scandinaves","author":"Skolem Thoralf","year":"1934","unstructured":"ThoralfSkolem. 1934. Ein verfahren zur behandlung gewisser exponentialer gleichungen. In Comptes Rendus du Congr\u00e8s des Math\u00e9maticiens Scandinaves."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704632","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704632","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:58Z","timestamp":1750295878000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704632"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,27]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,4,30]]}},"alternative-id":["10.1145\/3704632"],"URL":"https:\/\/doi.org\/10.1145\/3704632","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2025,3,27]]},"assertion":[{"value":"2024-02-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}