{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:46:50Z","timestamp":1777348010503,"version":"3.51.4"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452360","type":"print"},{"value":"9783030452377","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T00:00:00Z","timestamp":1587081600000},"content-version":"vor","delay-in-days":107,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We consider the decidability of the verification problem of programs <jats:italic>modulo axioms<\/jats:italic> \u2014 automatically verifying whether programs satisfy their assertions, when the function and relation symbols are interpreted as arbitrary functions and relations that satisfy a set of first-order axioms. Though verification of uninterpreted programs (with no axioms) is already undecidable, a recent work introduced a subclass of <jats:italic>coherent<\/jats:italic> uninterpreted programs, and showed that they admit decidable verification\u00a0[26]. We undertake a systematic study of various natural axioms for relations and functions, and study the decidability of the coherent verification problem. Axioms include relations being reflexive, symmetric, transitive, or total order relations, functions restricted to being associative, idempotent or commutative, and combinations of such axioms as well. Our comprehensive results unearth a rich landscape that shows that though several axiom classes admit decidability for coherent programs, coherence is not a panacea as several others continue to be undecidable.<\/jats:p>","DOI":"10.1007\/978-3-030-45237-7_10","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"158-177","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["What\u2019s Decidable About Program Verification Modulo Axioms?"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: Reveal: A formal verification tool for verilog designs. In: Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. pp. 343\u2013352. LPAR \u201908, Springer-Verlag, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-89439-1_25"},{"key":"10_CR2","unstructured":"Babi\u0107, D., Hu, A.J.: Structural Abstraction of Software Verification Conditions. In: Proceedings of the 19th Int. Conf. on Computer Aided Verification (CAV\u201907), Berlin, Germany. Lecture Notes in Computer Science, Springer (July 2007)"},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Babic, D., Hu, A.J.: Calysto: Scalable and precise extended static checking. In: Proceedings of the 30th International Conference on Software Engineering. p. 211-220. ICSE \u201908, Association for Computing Machinery, New York, NY, USA (2008). https:\/\/doi.org\/10.1145\/1368088.1368118","DOI":"10.1145\/1368088.1368118"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Proceedings of the 14th International Conference on Computer Aided Verification. pp. 78\u201392. CAV \u201902, Springer-Verlag, London, UK (2002)","DOI":"10.1007\/3-540-45657-0_7"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bueno, D., Sakallah, K.A.: euforia: Complete software model checking with uninterpreted functions. In: Enea, C., Piskac, R. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 363\u2013385. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-11245-5_17"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Proceedings of the 6th International Conference on Computer Aided Verification. pp. 68\u201380. CAV \u201994, Springer-Verlag, London, UK (1994)","DOI":"10.1007\/3-540-58179-0_44"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, A.K., Ibsen-Jensen, R., Pavlogiannis, A.: Algorithms for algebraic path properties in concurrent systems of constant treewidth components. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 733\u2013747. POPL \u201916, ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2837614.2837624","DOI":"10.1145\/2837614.2837624"},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A., Goyal, P.: Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. In: Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 97\u2013109. POPL \u201915, ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2676726.2676979","DOI":"10.1145\/2676726.2676979"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Doumane, A., Kuperberg, D., Pous, D., Pradic, P.: Kleene algebra with hypotheses. In: Boja\u0144czyk, M., Simpson, A. (eds.) Foundations of Software Science and Computation Structures. pp. 207\u2013223. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-17127-8_12"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 129\u2013142. POPL \u201913, ACM, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2429069.2429086","DOI":"10.1145\/2429069.2429086"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proofs that count. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 151\u2013164. POPL \u201914, ACM, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2535838.2535885","DOI":"10.1145\/2535838.2535885"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proof spaces for unbounded parallelism. In: Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 407\u2013420. POPL \u201915, ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2676726.2677012","DOI":"10.1145\/2676726.2677012"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Godoy, G., Tiwari, A.: Invariant checking for programs with procedure calls. In: Proceedings of the 16th International Symposium on Static Analysis. pp. 326\u2013342. SAS \u201909, Springer-Verlag, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-03237-0_22"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Assertion checking unified. In: Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation. pp. 363\u2013377. VMCAI\u201907, Springer-Verlag, Berlin, Heidelberg (2007)","DOI":"10.1007\/978-3-540-69738-1_26"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Proceedings of the 16th International Symposium on Static Analysis. pp. 69\u201385. SAS \u201909, Springer-Verlag, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 471\u2013482. POPL \u201910, ACM, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1706299.1706353","DOI":"10.1145\/1706299.1706353"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification. pp. 36\u201352. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Ho, Y.S., Mishchenko, A., Brayton, R.: Property directed reachability with word-level abstraction. In: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design. pp. 132\u2013139. FMCAD \u201917, FMCAD Inc, Austin, TX (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102251","DOI":"10.23919\/FMCAD.2017.8102251"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Hojati, R., Isles, A., Kirkpatrick, D., Brayton, R.K.: Verification using uninterpreted functions and finite instantiations. In: Srivas, M., Camilleri, A. (eds.) Formal Methods in Computer-Aided Design. pp. 218\u2013232. Springer Berlin Heidelberg, Berlin, Heidelberg (1996)","DOI":"10.1007\/BFb0031810"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Lahav, O., Nanevski, A., Sagiv, M.: Modular reasoning about heap paths via effectively propositional formulas. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 385\u2013396. POPL \u201914, ACM, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2535838.2535854","DOI":"10.1145\/2535838.2535854"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Kleene algebra with tests and commutativity conditions. In: Margaria, T., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 14\u201333. Springer Berlin Heidelberg, Berlin, Heidelberg (1996)","DOI":"10.1007\/3-540-61042-1_35"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427\u2013443 (May 1997). https:\/\/doi.org\/10.1145\/256167.256195","DOI":"10.1145\/256167.256195"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Kozen, D., Mamouras, K.: Kleene algebra with equations. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) Automata, Languages, and Programming. pp. 280\u2013292. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)","DOI":"10.1007\/978-3-662-43951-7_24"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Lewis, H.: Complexity results for classes of quantificational formulas. Journal of Computer and System Sciences 21(3), 317\u2013353 (1980)","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 283\u2013294. POPL \u201911, ACM, New York, NY, USA (2011). https:\/\/doi.org\/10.1145\/1926385.1926419","DOI":"10.1145\/1926385.1926419"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Mathur, U., Madhusudan, P., Viswanathan, M.: Decidable verification of uninterpreted programs. Proc. ACM Program. Lang. 3(POPL), 46:1\u201346:29 (Jan 2019). https:\/\/doi.org\/10.1145\/3290359","DOI":"10.1145\/3290359"},{"key":"10_CR27","unstructured":"Mathur, U., Madhusudan, P., Viswanathan, M.: What\u2019s decidable about program verification modulo axioms? CoRR abs\/1910.10889 (2019), http:\/\/arxiv.org\/abs\/1910.10889"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Mathur, U., Murali, A., Krogmeier, P., Madhusudan, P., Viswanathan, M.: Deciding memory safety for single-pass heap-manipulating programs. Proc. ACM Program. Lang. 4(POPL) (Dec 2019). https:\/\/doi.org\/10.1145\/3371103","DOI":"10.1145\/3371103"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Modular specification and verification of a cache-coherent interface. In: Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design. pp. 109\u2013116. FMCAD \u201916, FMCAD Inc, Austin, TX (2016)","DOI":"10.1109\/FMCAD.2016.7886668"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"McMillan, K.L., Padon, O.: Deductive verification in decidable fragments with ivy. In: Podelski, A. (ed.) Static Analysis. pp. 43\u201355. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-319-99725-4_4"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., R\u00fcthing, O., Seidl, H.: Checking herbrand equalities and beyond. In: Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation. pp. 79\u201396. VMCAI\u201905, Springer-Verlag, Berlin, Heidelberg (2005)","DOI":"10.1007\/978-3-540-30579-8_6"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Padon, O., Immerman, N., Shoham, S., Karbyshev, A., Sagiv, M.: Decidability of inferring inductive invariants. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 217\u2013231. POPL \u201916, ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2837614.2837640","DOI":"10.1145\/2837614.2837640"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made epr: Decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA), 108:1\u2013108:31 (Oct 2017). https:\/\/doi.org\/10.1145\/3140568","DOI":"10.1145\/3140568"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: Safety verification by interactive generalization. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 614\u2013630. PLDI \u201916, ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"10_CR35","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Strichman, O.: Reduced functional consistency of uninterpreted functions. Electron. Notes Theor. Comput. Sci. 144(2), 53\u201365 (Jan 2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.12.006","DOI":"10.1016\/j.entcs.2005.12.006"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Post, E.L.: Recursive unsolvability of a problem of thue. J. Symbolic Logic 12(1), 1\u201311 (03 1947)","DOI":"10.2307\/2267170"},{"key":"10_CR37","doi-asserted-by":"crossref","unstructured":"Ramsey, F.P.: On a Problem of Formal Logic, pp. 1\u201324. Birkh\u00e4user Boston, Boston, MA (1987)","DOI":"10.1007\/978-0-8176-4842-8_1"},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"Robertson, N., Seymour, P.D.: Graph minors. i. excluding a forest. Journal of Combinatorial Theory, Series B 35(1), 39\u201361 (1983)","DOI":"10.1016\/0095-8956(83)90079-5"},{"key":"10_CR39","doi-asserted-by":"publisher","unstructured":"Taube, M., Losa, G., McMillan, K.L., Padon, O., Sagiv, M., Shoham, S., Wilcox, J.R., Woos, D.: Modularity for decidability of deductive verification with applications to distributed systems. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 662\u2013677. PLDI 2018, ACM, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3192366.3192414","DOI":"10.1145\/3192366.3192414"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45237-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:04:48Z","timestamp":1616436288000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45237-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452360","9783030452377"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45237-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"155","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":"40","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":"8","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":"26% - 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":"14","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":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","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)"}}]}}