Type-based data structure verification

ABSTRACT

We present a refinement type-based approach for the static verification of complex data structure invariants. Our approach is based on the observation that complex data structures are typically fashioned from two elements: recursion (e.g., lists and trees), and maps (e.g., arrays and hash tables). We introduce two novel type-based mechanisms targeted towards these elements: recursive refinements and polymorphic refinements. These mechanisms automate the challenging work of generalizing and instantiating rich universal invariants by piggybacking simple refinement predicates on top of types, and carefully dividing the labor of analysis between the type system and an SMT solver. Further, the mechanisms permit the use of the abstract interpretation framework of liquid type inference to automatically synthesize complex invariants from simple logical qualifiers, thereby almost completely automating the verification. We have implemented our approach in dsolve, which uses liquid types to verify ocaml programs. We present experiments that show that our type-based approach reduces the manual annotation required to verify complex properties like sortedness, balancedness, binary-search-ordering, and acyclicity by more than an order of magnitude.

REFERENCES

• 1: Andrew W. Appel, SSA is functional programming, ACM SIGPLAN Notices, v.33 n.4, p.17-20, April 1998 [doi>10.1145/278283.278285]
• 2: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 3: Bor-Yuh Evan Chang , Xavier Rival, Relational inductive shape analysis, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 4: S. Cui, K. Donnelly, and H. Xi. Ats: A language that combines programming with theorem proving. In FroCos, 2005.
• 5: Luca de Alfaro. Vec: Extensible, functional arrays for ocaml. http://www.dealfaro.com/vec.html.
• 6: L. de Moura and N. Bjørner. Z3: An efficient smt solver. In TACAS, pages 337--340, 2008.
• 7: Joshua Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 2007.
• 8: J.C. Filliâtre. Ocaml software. http://www.lri.fr/ filliatr/software.en.html.
• 9: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA
• 10: Sumit Gulwani , Bill McCloskey , Ashish Tiwari, Lifting abstract interpreters to quantified logical domains, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 11: Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
• 12: Ranjit Jhala , Rupak Majumdar, Bit level types for high level reasoning, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181791]
• 13: Shuvendu Lahiri , Shaz Qadeer, Back to the future: revisiting precise program verification using SMT solvers, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 14: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 15: John McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962.
• 16: Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
• 17: A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Reasoning with the awkward squad. In ICFP, 2008. C. Okasaki. Purely Functional Data Structures. CUP, 1999.
• 18: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 19: Yann Régis-Gianas , François Pottier, A Hoare Logic for Call-by-Value Functional Programs, Proceedings of the 9th international conference on Mathematics of Program Construction, p.305-335, July 15-18, 2008, Marseille, France [doi>10.1007/978-3-540-70594-9_17]
• 20: Ming Kawaguchi , Patrick Rondon , Ranjit Jhala, Type-based data structure verification, Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation, June 15-21, 2009, Dublin, Ireland
• 21: Patrick M. Rondon , Ming Kawaguci , Ranjit Jhala, Liquid types, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 22: H. Xi. DML code examples. http://www.cs.bu.edu/fac/hwxi/DML/.
• 23: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]
• 24: Hongseok Yang , Oukseh Lee , Josh Berdine , Cristiano Calcagno , Byron Cook , Dino Distefano , Peter O'Hearn, Scalable Shape Analysis for Systems Code, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_36]
• 25: Karen Zee , Viktor Kuncak , Martin Rinard, Full functional verification of linked data structures, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Languages, Reliability, Verification

Keywords:
dependent types, hindley-milner, predicate abstraction, type inference