×

What’s decidable about program verification modulo axioms? (English) Zbl 1483.68200

Biere, Armin (ed.) et al., Tools and algorithms for the construction and analysis of systems. 26th international conference, TACAS 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12079, 158-177 (2020).
Summary: 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 [the authors, “Decidable verification of uninterpreted programs”, Proc. ACM Program. Lang. 3, No. POPL, Article No. 46, 29 p. (2019; doi:10.1145/3290359)]. 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.
For the entire collection see [Zbl 1471.68010].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

Reveal
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] 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) · Zbl 1511.68165
[2] 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
[3] Robertson, N., Seymour, P.D.: Graph minors. i. excluding a forest. Journal of Combinatorial Theory, Series B 35(1), 39-61 (1983) · Zbl 0521.05062
[4] Ramsey, F.P.: On a Problem of Formal Logic, pp. 1-24. Birkhäuser Boston, Boston, MA (1987)
[5] Post, E.L.: Recursive unsolvability of a problem of thue. J. Symbolic Logic 12(1), 1-11 (03 1947) · Zbl 1263.03030
[6] 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 · Zbl 1272.03071
[7] 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
[8] 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
[9] 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 · Zbl 1347.68234
[10] 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) · Zbl 1112.68094
[11] 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)
[12] 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
[13] 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
[14] 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 · Zbl 1284.68358
[15] Lewis, H.: Complexity results for classes of quantificational formulas. Journal of Computer and System Sciences 21(3), 317-353 (1980) · Zbl 0471.03034
[16] 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) · Zbl 1409.68179
[17] Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427-443 (May 1997). https://doi.org/10.1145/256167.256195 · Zbl 0882.03064
[18] 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)
[19] 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 · Zbl 1284.68403
[20] 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)
[21] 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
[22] 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)
[23] 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 · Zbl 1312.68059
[24] 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) · Zbl 1248.68146
[25] 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) · Zbl 1132.68470
[26] 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) · Zbl 1248.68143
[27] 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 · Zbl 1345.68102
[28] 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 · Zbl 1284.68395
[29] 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 · Zbl 1301.68178
[30] 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) · Zbl 1524.68201
[31] 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 · Zbl 1346.68047
[32] 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 · Zbl 1347.68260
[33] 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)
[34] 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) · Zbl 1522.68299
[35] 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) · Zbl 1010.68522
[36] 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
[37] 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) · Zbl 1135.68463
[38] 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) · Zbl 1182.68111
[39] 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
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.