Philippe Suter
Viktor Kuncak
ABSTRACT
We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term algebra homomorphisms) mapping algebraic data type values into values in other decidable theories (e.g. sets, multisets, lists, integers, booleans). Each instance of our decision procedure family is sound; we identify a widely applicable many-to-one condition on abstraction functions that implies the completeness. Complete instances of our decision procedure include the following correctness statements: 1) a functional data structure implementation satisfies a recursively specified invariant, 2) such data structure conforms to a contract given in terms of sets, multisets, lists, sizes, or heights, 3) a transformation of a formula (or lambda term) abstract syntax tree changes the set of free variables in the specified way.
- F. Baader and S. Ghilardi. Connecting many-sorted theories. In CADE, pages 278--294, 2005. Google Scholar
Digital Library
- F. Baader and W. Snyder. Unification theory. In Handbook of Automated Reasoning. Elsevier, 2001.Google ScholarCross Ref
- M. Barnett, K.R.M. Leino, and W. Schulte. The Spec# programming system: An overview. In CASSIS: Int. Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices, 2004. Google ScholarDigital Library
- C. Barrett, S. Ranise, A. Stump, and C. Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). http://www.SMT-LIB.org, 2009.Google Scholar
- C. Barrett, I. Shikanian, and C. Tinelli. An abstract decision procedure for satisfiability in the theory of recursive data types. Electronic Notes in Theoretical Computer Science, 174(8):23--37, 2007. Google ScholarDigital Library
- C. Barrett and C. Tinelli. CVC3. In CAV, 2007. Google ScholarDigital Library
- B. Beckert, R. Hähnle, and P.H. Schmitt, editors. Verification of Object-Oriented Software: The KeY Approach. LNCS 4334. Springer, 2007. Google ScholarDigital Library
- N. Bjørner, N. Tillmann, and A. Voronkov. Path feasibility analysis for string-manipulating programs. In TACAS, pages 307--321, 2009. Google ScholarDigital Library
- E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer-Verlag, 1997.Google ScholarCross Ref
- C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on Java predicates. In ISSTA, 2002. Google ScholarDigital Library
- A.R. Bradley and Z. Manna. The Calculus of Computation. Springer, 2007.Google Scholar
- R. Cartwright and M. Fagan. Soft typing. In PLDI, 1991. Google ScholarDigital Library
- K. Claessen and J. Hughes. Quickcheck: a lightweight tool for random testing of haskell programs. In ICFP, pages 268--279, 2000. Google ScholarDigital Library
- E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent c. In TPHOLs, 2009. Google ScholarDigital Library
- H. Comon and C. Delor. Equational formulae with membership constraints. Information and Computation, 112(2):167--216, 1994. Google ScholarDigital Library
- L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, pages 337--340, 2008. Google ScholarDigital Library
- L. de Moura and N. Bjørner. Generalized, efficient array decision procedures. In FMCAD, 2009.Google ScholarCross Ref
- J. Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, 2007. CMU-CS-07-129.Google Scholar
- J. Dunfield and F. Pfenning. Tridirectional typechecking. In POPL, pages 281--292, 2004. Google ScholarDigital Library
- P. Fontaine. Combinations of theories and the Bernays-Schönfinkel-Ramsey class. In VERIFY, 2007.Google Scholar
- H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast decision procedures. In CAV, 2004.Google Scholar
- S. Ghilardi. Model theoretic methods in combined constraint satisfiability. J. Automated Reasoning, 33(3-4):221--249, 2005. Google ScholarDigital Library
- M. Gligoric, T. Gvero, V. Jagannath, S. Khurshid, V. Kuncak, and D. Marinov. On test generation through programming in UDITA. Technical Report LARA-REPORT-2009-05, EPFL, Sep. 2009.Google Scholar
- C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271--281, 1971.Google ScholarDigital Library
- W. Hodges. Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.Google Scholar
- P.F. Hoogendijk and R.C. Backhouse. Relational programming laws in the tree, list, bag, set hierarchy. Sci. Comput. Program., 22(1-2), 1994. Google ScholarDigital Library
- C. Ihlemann, S. Jacobs, and V. Sofronie-Stokkermans. On local reasoning in verification. In TACAS, pages 265--281, 2008. Google ScholarDigital Library
- J. Jaffar. Minimal and complete word unification. Journal of the ACM, 37(1):47--85, 1990. Google ScholarDigital Library
- M. Kawaguchi, P.M. Rondon, and R. Jhala. Type-based data structure verification. In PLDI, pages 304--315, 2009. Google ScholarDigital Library
- S. Krstić, A. Goel, J. Grundy, and C. Tinelli. Combined satisfiability modulo parametric theories. In TACAS, 2007. Google ScholarDigital Library
- V. Kuncak. Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology, February 2007. Google ScholarDigital Library
- V. Kuncak, P. Lam, K. Zee, and M. Rinard. Modular pluggable analyses for data structure consistency. IEEE Transactions on Software Engineering, 32(12), December 2006. Google ScholarDigital Library
- V. Kuncak, H.H. Nguyen, and M. Rinard. Deciding boolean algebra with presburger arithmetic. J. Automated Reasoning, 2006. Google ScholarDigital Library
- V. Kuncak and M. Rinard. Structural subtyping of non-recursive types is decidable. In LICS, 2003. Google ScholarDigital Library
- V. Kuncak and M. Rinard. Decision procedures for set-valued fields. In International Workshop on Abstract Interpretation of Object-Oriented Languages, 2005.Google ScholarDigital Library
- V. Kuncak and M. Rinard. Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In CADE, 2007. Google ScholarDigital Library
- S. Lahiri and S. Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In POPL, 2008. Google ScholarDigital Library
- S.K. Lahiri and S. Qadeer. Verifying properties of well-founded linked lists. In POPL, 2006. Google ScholarDigital Library
- P. Lam, V. Kuncak, and M. Rinard. Generalized typestate checking for data structure consistency. In VMCAI, 2005. Google ScholarDigital Library
- P. Maier. Deciding extensions of the theories of vectors and bags. In VMCAI, 2009. Google ScholarDigital Library
- G. Makanin. The problem of solvability of equations in a free semigroup. Math. USSR Sbornik, pages 129--198, 1977. (In AMS, (1979)).Google ScholarCross Ref
- A.I. Mal'cev. Chapter 23: Axiomatizable classes of locally free algebras of various types. In The Metamathematics of Algebraic Systems, volume 66. North Holland, 1971.Google Scholar
- Z. Manna, H.B. Sipma, and T. Zhang. Verifying balanced trees. In LFCS, pages 363--378, 2007. Google ScholarDigital Library
- J. McCarthy. Recursive functions of symbolic expressions and their computation by machine, part 1. Comm. A.C.M., 3:184--195, 1960. Google ScholarDigital Library
- S. McPeak and G.C. Necula. Data structure specifications via local equality axioms. In CAV, pages 476--490, 2005. Google ScholarDigital Library
- E. Meijer, M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In FPCA, volume 523 of LNCS, 1991. Google ScholarDigital Library
- A. Møller and M.I. Schwartzbach. The Pointer Assertion Logic Engine. In Proc. PLDI, 2001. Google ScholarDigital Library
- G. Nelson and D.C. Oppen. Simplification by cooperating decision procedures. TOPLAS, 1(2):245--257, 1979. Google ScholarDigital Library
- G. Nelson and D.C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27(2):356--364, 1980. Google ScholarDigital Library
- H.H. Nguyen, C. David, S. Qin, and W.-N. Chin. Automated verification of shape, size and bag properties via separation logic. In VMCAI, 2007. Google ScholarDigital Library
- M. Odersky, L. Spoon, and B. Venners. Programming in Scala: a comprehensive step-by-step guide. Artima Press, 2008. Google ScholarDigital Library
- C. Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998. Google ScholarDigital Library
- D.C. Oppen. Reasoning about recursively defined data structures. In POPL, pages 151--157, 1978. Google ScholarDigital Library
- C.H. Papadimitriou. On the complexity of integer programming. Journal of the ACM, 28(4):765--768, 1981. Google ScholarDigital Library
- R. Piskac and V. Kuncak. Decision procedures for multisets with cardinality constraints. In VMCAI, number 4905 in LNCS, 2008. Google ScholarDigital Library
- R. Piskac and V. Kuncak. Linear arithmetic with stars. In CAV, 2008. Google ScholarDigital Library
- W. Plandowski. Satisfiability of word equations with constants is in PSPACE. Journal of the ACM, 51(3), 2004. Google ScholarDigital Library
- J.A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1), 1965. Google ScholarDigital Library
- P.M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI, pages 159--169, 2008. Google ScholarDigital Library
- T. Rybina and A. Voronkov. A decision procedure for term algebras with queues. ACM Transactions on Computational Logic (TOCL), 2(2):155--181, 2001. Google ScholarDigital Library
- V. Sofronie-Stokkermans. Locality results for certain extensions of theories with bridging functions. In CADE, 2009. Google ScholarDigital Library
- C. Tinelli and C. Zarba. Combining nonstably infinite theories. Journal of Automated Reasoning, 34(3), 2005. Google ScholarDigital Library
- D. Walker and G. Morrisett. Alias types for recursive data structures. In Workshop on Types in Compilation, 2000. Google ScholarDigital Library
- T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard. Field constraint analysis. In VMCAI, 2006. Google ScholarDigital Library
- T. Wies, R. Piskac, and V. Kuncak. Combining theories with shared set operations. In FroCoS: Frontiers in Combining Systems, 2009. Google ScholarDigital Library
- H. Xi. Dependently typed pattern matching. Journal of Universal Computer Science, 9(8):851--872, 2003.Google Scholar
- K. Zee, V. Kuncak, and M. Rinard. Full functional verification of linked data structures. In PLDI, 2008. Google ScholarDigital Library
- T. Zhang, H.B. Sipma, and Z. Manna. The decidability of the first-order theory of Knuth-Bendix order. In CADE, 2005. Google ScholarDigital Library
- T. Zhang, H.B. Sipma, and Z. Manna. Decision procedures for term algebras with integer constraints. Inf. Comput., 204(10):1526--1574, 2006. Google ScholarDigital Library
- D. Zhu and H. Xi. Safe programming with pointers through stateful views. In PADL, 2005. Google ScholarDigital Library
Index Terms
- Decision procedures for algebraic data types with abstractions
Recommendations
Decision procedures for algebraic data types with abstractions
POPL '10We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (...
Reasoning About Algebraic Data Types with Abstractions
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 ...
Polymorphic algebraic data type reconstruction
PPDP '06: Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programmingOne of the disadvantages of statically typed languages is the programming overhead caused by writing all the necessary type information: Both type declarations and type definitions are typically required. Traditional type inference aims at relieving the ...
Comments