×

Reasoning about algebraic data types with abstractions. (English) Zbl 1386.68104

Summary: Reasoning about functions that operate over algebraic data types is an important problem for a large variety of applications. One application of particular interest is network applications that manipulate or reason about complex message structures, such as XML messages. This paper presents a decision procedure for reasoning about algebraic data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types to values in a decidable domain. We show that the procedure is sound and complete for a class of catamorphisms that satisfy a generalized sufficient surjectivity condition. Our work extends a previous decision procedure that unrolls catamorphism functions until a solution is found. We use the generalized sufficient surjectivity condition to address an incompleteness in the previous unrolling algorithm (and associated proof). We then propose the categories of monotonic and associative catamorphisms, which we argue provide a more intuitive inclusion test than the generalized sufficient surjectivity condition. We use these notions to address two open problems from previous work: (1) we provide a bound, with respect to formula size, on the number of unrollings necessary for completeness, showing that it is linear for monotonic catamorphisms and exponentially small for associative catamorphisms, and (2) we demonstrate that associative catamorphisms can be combined within a formula while preserving completeness. Our combination results extend the set of problems that can be reasoned about using the catamorphism-based approach. We also describe an implementation of the approach, called RADA, which accepts formulas in an extended version of the SMT-LIB 2.0 syntax. The procedure is quite general and is central to the reasoning infrastructure for Guardol, a domain-specific language for reasoning about network guards.

MSC:

68Q65 Abstract data types; algebraic specification
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, pp. 171-177 (2011) · Zbl 1277.68132
[2] Barrett, C; Shikanian, I; Tinelli, C, An abstract decision procedure for satisfiability in the theory of recursive data types, Electron. Notes Theor. Comput. Sci., 174, 23-37, (2007) · Zbl 1277.68132
[3] Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: SMT (2010)
[4] Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the leon verification system: verification by translation to recursive functions. In: SCALA, pp. 1:1-1:10 (2013)
[5] Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: TACAS, pp. 150-153 (2010)
[6] De Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: TACAS, pp. 337-340 (2008)
[7] Flajolet, P., Sedgewick, R.: Analytic Combinatorics. Cambridge University Press, Cambridge (2009) · Zbl 1165.05001
[8] Hardin, D., Slind, K., Whalen, M., Pham, T.H.: The guardol language and verification system. In: TACAS, pp. 18-32 (2012)
[9] Jacobs, S., Kuncak, V.: Towards Complete Reasoning about Axiomatic Specifications. In: VMCAI, pp. 278-293 (2011) · Zbl 1317.68117
[10] Kaufmann, M., Manolios, P., Moore, J.: Computer-Aided Reasoning: ACL2 Case Studies. Springer, Heidelberg (2000)
[11] Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: PLDI, pp. 222-233 (2011)
[12] Koshy, T.: Catalan Numbers with Applications. Oxford University Press, Oxford (2009) · Zbl 1159.05001
[13] Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: LPAR, pp. 348-370 (2010) · Zbl 1253.68095
[14] Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL, pp. 611-622 (2011) · Zbl 1284.68411
[15] Madhusudan, P., Qiu, X., Stefanescu, A.: Recursive proofs for inductive tree data-structures. In: POPL, pp. 123-136 (2012) · Zbl 1321.68226
[16] Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002) · Zbl 0994.68131
[17] Oppen, DC, Reasoning about recursively defined data structures, J. ACM, 27, 403-411, (1980) · Zbl 0477.68025
[18] Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: CADE, pp. 748-752 (1992) · Zbl 0477.68025
[19] Pham, T.H.: Verification of recursive data types using abstractions. Ph.D. thesis, University of Minnesota (2014)
[20] Pham, T.H., Whalen, M.: An improved unrolling-based decision procedure for algebraic data types. In: VSTTE (2013)
[21] Pham, T.H., Whalen, M.W.: Parameterized abstractions for reasoning about algebraic data types. In: CFV (2013). Available at http://www-users.cs.umn.edu/ hung/papers/cfv13
[22] Pham, T.H., Whalen, M.W.: RADA: A tool for reasoning about algebraic data types with abstractions. In: ESEC/SIGSOFT FSE, pp. 611-614 (2013)
[23] Reynolds, A., Kuncak, V., Induction for SMT Solvers. In: VMCAI, (2015) · Zbl 1432.68418
[24] Sato, R., Unno, H., Kobayashi, N.: Towards a Scalable Software Model Checker for Higher-Order Programs. In: PEPM, pp. 53-62 (2013)
[25] Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: CADE, pp. 67-83 (2009) · Zbl 1250.03022
[26] Stanley, R.P.: Enumerative Combinatorics, vol. 2. Cambridge University Press, Cambridge (2001) · Zbl 0978.05002
[27] Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL, pp. 199-210 (2010) · Zbl 1312.68147
[28] Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: SAS (2011) · Zbl 1317.68124
[29] Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: PLDI, pp. 349-361 (2008)
[30] Zee, K., Kuncak, V., Rinard, M.C.: An integrated proof language for imperative programs. In: PLDI, pp. 338-351 (2009)
[31] Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for term algebras with integer constraints. In: Information and Computation, pp. 152-167 (2004) · Zbl 1126.68585
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.