Abstract
We consider the decidability of the verification problem of programs modulo axioms — 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 coherent uninterpreted programs, and showed that they admit decidable verification [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.
Umang Mathur is partially supported by a Google PhD Fellowship. P. Madhusudan is partially supported by NSF CCF 1527395. Mahesh Viswanathan is partially supported by NSF CCF 1901069
Chapter PDF
Similar content being viewed by others
References
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–352. LPAR ’08, Springer-Verlag, Berlin, Heidelberg (2008)
Babić, D., Hu, A.J.: Structural Abstraction of Software Verification Conditions. In: Proceedings of the 19th Int. Conf. on Computer Aided Verification (CAV’07), Berlin, Germany. Lecture Notes in Computer Science, Springer (July 2007)
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 ’08, Association for Computing Machinery, New York, NY, USA (2008). https://doi.org/10.1145/1368088.1368118
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–92. CAV ’02, Springer-Verlag, London, UK (2002)
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–385. Springer International Publishing, Cham (2019)
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–80. CAV ’94, Springer-Verlag, London, UK (1994)
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–747. POPL ’16, ACM, New York, NY, USA (2016). https://doi.org/10.1145/2837614.2837624
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–109. POPL ’15, ACM, New York, NY, USA (2015). https://doi.org/10.1145/2676726.2676979
Doumane, A., Kuperberg, D., Pous, D., Pradic, P.: Kleene algebra with hypotheses. In: Bojańczyk, M., Simpson, A. (eds.) Foundations of Software Science and Computation Structures. pp. 207–223. Springer International Publishing, Cham (2019)
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–142. POPL ’13, ACM, New York, NY, USA (2013). https://doi.org/10.1145/2429069.2429086
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–164. POPL ’14, ACM, New York, NY, USA (2014). https://doi.org/10.1145/2535838.2535885
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–420. POPL ’15, ACM, New York, NY, USA (2015). https://doi.org/10.1145/2676726.2677012
Godoy, G., Tiwari, A.: Invariant checking for programs with procedure calls. In: Proceedings of the 16th International Symposium on Static Analysis. pp. 326–342. SAS ’09, Springer-Verlag, Berlin, Heidelberg (2009)
Gulwani, S., Tiwari, A.: Assertion checking unified. In: Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation. pp. 363–377. VMCAI’07, Springer-Verlag, Berlin, Heidelberg (2007)
Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Proceedings of the 16th International Symposium on Static Analysis. pp. 69–85. SAS ’09, Springer-Verlag, Berlin, Heidelberg (2009)
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–482. POPL ’10, ACM, New York, NY, USA (2010). https://doi.org/10.1145/1706299.1706353
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–52. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)
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–139. FMCAD ’17, FMCAD Inc, Austin, TX (2017). https://doi.org/10.23919/FMCAD.2017.8102251
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–232. Springer Berlin Heidelberg, Berlin, Heidelberg (1996)
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–396. POPL ’14, ACM, New York, NY, USA (2014). https://doi.org/10.1145/2535838.2535854
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–33. Springer Berlin Heidelberg, Berlin, Heidelberg (1996)
Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (May 1997). https://doi.org/10.1145/256167.256195
Kozen, D., Mamouras, K.: Kleene algebra with equations. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) Automata, Languages, and Programming. pp. 280–292. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)
Lewis, H.: Complexity results for classes of quantificational formulas. Journal of Computer and System Sciences 21(3), 317–353 (1980)
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–294. POPL ’11, ACM, New York, NY, USA (2011). https://doi.org/10.1145/1926385.1926419
Mathur, U., Madhusudan, P., Viswanathan, M.: Decidable verification of uninterpreted programs. Proc. ACM Program. Lang. 3(POPL), 46:1–46:29 (Jan 2019). https://doi.org/10.1145/3290359
Mathur, U., Madhusudan, P., Viswanathan, M.: What’s decidable about program verification modulo axioms? CoRR abs/1910.10889 (2019), http://arxiv.org/abs/1910.10889
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
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–116. FMCAD ’16, FMCAD Inc, Austin, TX (2016)
McMillan, K.L., Padon, O.: Deductive verification in decidable fragments with ivy. In: Podelski, A. (ed.) Static Analysis. pp. 43–55. Springer International Publishing, Cham (2018)
Müller-Olm, M., Rüthing, O., Seidl, H.: Checking herbrand equalities and beyond. In: Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation. pp. 79–96. VMCAI’05, Springer-Verlag, Berlin, Heidelberg (2005)
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–231. POPL ’16, ACM, New York, NY, USA (2016). https://doi.org/10.1145/2837614.2837640
Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made epr: Decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA), 108:1–108:31 (Oct 2017). https://doi.org/10.1145/3140568
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–630. PLDI ’16, ACM, New York, NY, USA (2016). https://doi.org/10.1145/2908080.2908118
Pnueli, A., Strichman, O.: Reduced functional consistency of uninterpreted functions. Electron. Notes Theor. Comput. Sci. 144(2), 53–65 (Jan 2006). https://doi.org/10.1016/j.entcs.2005.12.006
Post, E.L.: Recursive unsolvability of a problem of thue. J. Symbolic Logic 12(1), 1–11 (03 1947)
Ramsey, F.P.: On a Problem of Formal Logic, pp. 1–24. Birkhäuser Boston, Boston, MA (1987)
Robertson, N., Seymour, P.D.: Graph minors. i. excluding a forest. Journal of Combinatorial Theory, Series B 35(1), 39–61 (1983)
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–677. PLDI 2018, ACM, New York, NY, USA (2018). https://doi.org/10.1145/3192366.3192414
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Mathur, U., Madhusudan, P., Viswanathan, M. (2020). What’s Decidable About Program Verification Modulo Axioms?. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12079. Springer, Cham. https://doi.org/10.1007/978-3-030-45237-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-45237-7_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45236-0
Online ISBN: 978-3-030-45237-7
eBook Packages: Computer ScienceComputer Science (R0)