{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:53:30Z","timestamp":1790927610705,"version":"4.1.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1422798, 1138994, 1527395, 1329991"],"award-info":[{"award-number":["1422798, 1138994, 1527395, 1329991"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>\n            We study the problem of completely automatically verifying uninterpreted programs\u2014programs that work over arbitrary data models that provide an interpretation for the constants, functions and relations the program uses. The verification problem asks whether a given program satisfies a postcondition written using quantifier-free formulas with equality on the final state, with no loop invariants, contracts, etc. being provided. We show that this problem is undecidable in general. The main contribution of this paper is a subclass of programs, called\n            <jats:italic>coherent programs<\/jats:italic>\n            that admits decidable verification, and can be decided in Pspace. We then extend this class of programs to classes of programs that are\n            <jats:italic>k<\/jats:italic>\n            -coherent, where\n            <jats:italic>k<\/jats:italic>\n            \u2208 \u2115, obtained by (automatically) adding\n            <jats:italic>k<\/jats:italic>\n            ghost variables and assignments that make them coherent. We also extend the decidability result to programs with recursive function calls and prove several undecidability results that show why our restrictions to obtain decidability seem necessary.\n          <\/jats:p>","DOI":"10.1145\/3290359","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Decidable verification of uninterpreted programs"],"prefix":"10.1145","volume":"3","author":[{"given":"Umang","family":"Mathur","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73561"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007390"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516518"},{"key":"e_1_2_2_5_1","volume-title":"Bradley and Zohar Manna","author":"Aaron","year":"2007","unstructured":"Aaron R. Bradley and Zohar Manna . 2007 . The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag , Berlin, Heidelberg. Aaron R. Bradley and Zohar Manna. 2007. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag, Berlin, Heidelberg."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371364"},{"key":"e_1_2_2_7_1","volume-title":"Proceedings of the 6th International Conference on Computer Aided Verification (CAV \u201994)","author":"Jerry","unstructured":"Jerry R. Burch and David L. Dill. 1994. Automatic Verification of Pipelined Microprocessor Control . In Proceedings of the 6th International Conference on Computer Aided Verification (CAV \u201994) . Springer-Verlag, London, UK, UK, 68\u201380. http:\/\/dl.acm.org\/citation.cfm?id=647763.735662 Jerry R. Burch and David L. Dill. 1994. Automatic Verification of Pipelined Microprocessor Control. In Proceedings of the 6th International Conference on Computer Aided Verification (CAV \u201994). Springer-Verlag, London, UK, UK, 68\u201380. http:\/\/dl.acm.org\/citation.cfm?id=647763.735662"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837624"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676979"},{"key":"e_1_2_2_10_1","volume-title":"Graph Structure and Monadic Second-Order Logic: A LanguageTheoretic Approach","author":"Courcelle Professor Bruno","unstructured":"Professor Bruno Courcelle and Dr Joost Engelfriet . 2012. Graph Structure and Monadic Second-Order Logic: A LanguageTheoretic Approach ( 1 st ed.). Cambridge University Press , New York, NY, USA . Professor Bruno Courcelle and Dr Joost Engelfriet. 2012. Graph Structure and Monadic Second-Order Logic: A LanguageTheoretic Approach (1st ed.). Cambridge University Press, New York, NY, USA.","edition":"1"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926407"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734087"},{"key":"e_1_2_2_13_1","volume-title":"Foundations of Software Science and Computation Structures","author":"Esparza Javier","unstructured":"Javier Esparza and Jens Knoop . 1999. An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis . In Foundations of Software Science and Computation Structures , Wolfgang Thomas (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 14\u201330. Javier Esparza and Jens Knoop. 1999. An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis. In Foundations of Software Science and Computation Structures, Wolfgang Thomas (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 14\u201330."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535885"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677012"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_16"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_22"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/111310.111320"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964030"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_17"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_19"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763048.1763086"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706353"},{"key":"e_1_2_2_25_1","volume-title":"Software Model Checking for People Who Love Automata","author":"Heizmann Matthias","unstructured":"Matthias Heizmann , Jochen Hoenicke , and Andreas Podelski . 2013. Software Model Checking for People Who Love Automata . In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 36\u201352. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2013. Software Model Checking for People Who Love Automata. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 36\u201352."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802201"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0366-1"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926419"},{"key":"e_1_2_2_32_1","volume-title":"Decidable Verification of Uninterpreted Programs. CoRR abs\/1811.00192","author":"Mathur Umang","year":"2018","unstructured":"Umang Mathur , P. Madhusudan , and Mahesh Viswanathan . 2018. Decidable Verification of Uninterpreted Programs. CoRR abs\/1811.00192 ( 2018 ). http:\/\/arxiv.org\/abs\/1811.00192 Umang Mathur, P. Madhusudan, and Mahesh Viswanathan. 2018. Decidable Verification of Uninterpreted Programs. CoRR abs\/1811.00192 (2018). http:\/\/arxiv.org\/abs\/1811.00192"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/800076.802477"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_6"},{"key":"e_1_2_2_35_1","volume-title":"A Note on Karr\u2019s Algorithm","author":"M\u00fcller-Olm Markus","unstructured":"Markus M\u00fcller-Olm and Helmut Seidl . 2004. A Note on Karr\u2019s Algorithm . In Automata, Languages and Programming, Josep D\u00edaz, Juhani Karhum\u00e4ki, Arto Lepist\u00f6, and Donald Sannella (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 1016\u20131028. Markus M\u00fcller-Olm and Helmut Seidl. 2004. A Note on Karr\u2019s Algorithm. In Automata, Languages and Programming, Josep D\u00edaz, Juhani Karhum\u00e4ki, Arto Lepist\u00f6, and Donald Sannella (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1016\u20131028."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_17"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0095-8956(83)90079-5"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90054-P"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290359","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290359","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290359","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290359"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":40,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290359"],"URL":"https:\/\/doi.org\/10.1145\/3290359","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}