Towards complete reasoning about axiomatic specifications. (English) Zbl 1317.68117

Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 278-293 (2011).
Summary: To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision procedures for reasoning about such universally quantified properties of functional programs, using local theory extension methodology. We establish new classes of universally quantified formulas whose satisfiability can be checked in a complete way by finite quantifier instantiation. These classes include single-invocation axioms that generalize standard function contracts, but also certain many-invocation axioms, specifying that functions satisfy congruence, injectivity, or monotonicity with respect to abstraction functions, as well as conjunctions of some of these properties. These many-invocation axioms can specify correctness of abstract data type implementations as well as certain information-flow properties. We also present a decidability-preserving construction that enables the same function to be specified using different classes of decidable specifications on different partitions of its domain.
For the entire collection see [Zbl 1206.68013].


68Q60 Specification and verification (program logics, model checking, etc.)
68N18 Functional programming and lambda calculus
68Q65 Abstract data types; algebraic specification


Full Text: DOI


[1] Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005) · Zbl 1176.68116 · doi:10.1007/11609773_28
[2] Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009) · doi:10.1007/978-3-642-03359-9_2
[3] Ge, Y., de Moura, L.: Complete instantiation for quantified SMT formulas. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009) · Zbl 1242.68280 · doi:10.1007/978-3-642-02658-4_25
[4] Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: International Conference on Software Engineering, ICSE (2010) · doi:10.1145/1806799.1806835
[5] Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008) · Zbl 1134.68410 · doi:10.1007/978-3-540-78800-3_19
[6] Jacobs, S.: Incremental instance generation in local reasoning. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 368–382. Springer, Heidelberg (2009) · Zbl 1242.68164 · doi:10.1007/978-3-642-02658-4_29
[7] Jacobs, S.: Hierarchic Decision Procedures for Verification. PhD thesis, Saarland University, Germany (2010)
[8] Jacobs, S., Kuncak, V.: On complete reasoning about axiomatic specifications. Technical Report EPFL-REPORT-151486, EPFL (2010) · Zbl 1317.68117
[9] Jacobs, S., Sofronie-Stokkermans, V.: Applications of hierarchical reasoning in the verification of complex systems. Electronic Notes in Theoretical Computer Science 174(8), 39–54 (2007) · Zbl 1277.68135 · doi:10.1016/j.entcs.2006.11.038
[10] Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking for data structure consistency. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 430–447. Springer, Heidelberg (2005) · Zbl 1111.68509 · doi:10.1007/978-3-540-30579-8_28
[11] McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 476–490. Springer, Heidelberg (2005) · Zbl 1081.68584 · doi:10.1007/11513988_47
[12] Podelski, A., Wies, T.: Counterexample-guided focus. In: 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (2010) · Zbl 1312.68067 · doi:10.1145/1706299.1706330
[13] Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 219–234. Springer, Heidelberg (2005) · Zbl 1135.03330 · doi:10.1007/11532231_16
[14] Sofronie-Stokkermans, V.: Efficient hierarchical reasoning about functions over numerical domains. In: Dengel, A.R., Berns, K., Breuel, T.M., Bomarius, F., Roth-Berghofer, T.R. (eds.) KI 2008. LNCS (LNAI), vol. 5243, pp. 135–143. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-85845-4_17
[15] Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 67–83. Springer, Heidelberg (2009) · Zbl 1250.03022 · doi:10.1007/978-3-642-02959-2_5
[16] Sofronie-Stokkermans, V., Ihlemann, C.: Automated reasoning in some local extensions of ordered structures. Journal of Multiple-Valued Logic and Soft Computing 13(4-6), 397–414 (2007) · Zbl 1137.03007
[17] Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (2010) · Zbl 1312.68147 · doi:10.1145/1706299.1706325
[18] Wies, T., Kuncak, V., Lam, P., Podelski, A., Rinard, M.: Field constraint analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 157–173. Springer, Heidelberg (2005) · Zbl 1176.68130 · doi:10.1007/11609773_11
[19] Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for recursive data structures with integer constraints. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 152–167. Springer, Heidelberg (2004) · Zbl 1126.68585 · doi:10.1007/978-3-540-25984-8_9
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.