Patrick M. Rondon
Abstract
We present Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without the heavy price of manual annotation. We have implemented liquid type inference in DSOLVE, which takes as input an OCAML program and a set of logical qualifiers and infers dependent types for the expressions in the OCAML program. To demonstrate the utility of our approach, we describe experiments using DSOLVE to statically verify the safety of array accesses on a set of OCAML benchmarks that were previously annotated with dependent types as part of the DML project. We show that when used in conjunction with a fixed set of array bounds checking qualifiers, DSOLVE reduces the amount of manual annotation required for proving safety from 31% of program text to under 1%.
- Tilak Agerwala and Jayadev Misra. Assertion graphs for verifying and synthesizing programs. Technical Report 83, University of Texas, Austin, 1978. Google Scholar
Digital Library
- L. Augustsson. Cayenne - a language with dependent types. In ICFP, 1998. Google ScholarDigital Library
- T. Ball and S.K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL, pages 1--3. ACM, 2002. Google ScholarDigital Library
- S. Chaki, E. M. Clarke, A. Groce, J. Ouaknine, O. Strichman, and K. Yorav. Efficient verification of sequential and concurrent c programs. FMSD, 25(2-3):129--166, 2004. Google ScholarDigital Library
- B. Chin, S. Markstrum, T. D. Millstein, and J. Palsberg. Inference of user-defined type qualifiers and qualifier rules. In ESOP, pages 264--278, 2006. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV, LNCS 1855, pages 154--169. Springer, 2000. Google ScholarDigital Library
- L. Damas and R. Milner. Principal type-schemes for functional programs. In POPL, 1982. Google ScholarDigital Library
- E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. Google ScholarDigital Library
- B. Dutertre and L. De Moura. Yices SMT solver. http://yices.csl.sri.com/.Google Scholar
- C. Flanagan. Hybrid type checking. In POPL. ACM, 2006. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In POPL. ACM, 2002. Google ScholarDigital Library
- C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In PLDI, 1993. Google ScholarDigital Library
- J.S. Foster. Type Qualifiers: Lightweight Specifications to Improve Software Quality. PhD thesis, U.C. Berkeley, 2002. Google ScholarDigital Library
- T. Freeman and F. Pfenning. Refinement types for ML. In PLDI, 1991. Google ScholarDigital Library
- S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In CAV, LNCS 1254, pages 72--83. Springer, 1997. Google ScholarDigital Library
- T.A. Henzinger, R. Jhala, R. Majumdar, and K.L. McMillan. Abstractions from proofs. In POPL 04. ACM, 2004. Google ScholarDigital Library
- F. Ivancic, I. Shlyakhter, A. Gupta, and M. K. Ganai. Model checking c programs using f-soft. In ICCD, pages 297--308, 2005. Google ScholarDigital Library
- K. Knowles and C. Flanagan. Type reconstruction for general refinement types. In ESOP, 2007. Google ScholarDigital Library
- P. Lincoln and J. C. Mitchell. Algorithmic aspects of type inference with subtypes. In POPL, Albequerque, New Mexico, 1992. Google ScholarDigital Library
- P. Martin-Lof. Constructive mathematics and computer programming. Royal Society of London Philosophical Transactions Series A, 312:501--518, October 1984.Google ScholarCross Ref
- G. Nelson. Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center, 1981.Google Scholar
- X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. Dynamic typing with dependent types. In IFIP TCS, pages 437--450, 2004.Google ScholarCross Ref
- F. Pottier. Simplifying subtyping constraints. In ICFP, New York, NY, USA, 1996. ACM Press. Google ScholarDigital Library
- P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. Technical Report CSE Tech Report, UCSD, 2008.Google ScholarDigital Library
- M. Sulzmann, M. Odersky, and M. Wehr. Type inference with constrained types. In FOOL, 1997.Google Scholar
- H. Xi. DML code examples. http://www.cs.bu.edu/fac/hwxi/DML/.Google Scholar
- H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In PLDI, 1998. Google ScholarDigital Library
- H. Xi and F. Pfenning. Dependent types in practical programming. In POPL, pages 214--227, 1999. Google ScholarDigital Library
- Y. Xie and A. Aiken. Scalable error detection using boolean satisfiability. In POPL, pages 351--363, 2005. Google ScholarDigital Library
Index Terms
- Liquid types
Recommendations
Liquid types
PLDI '08: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe present Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid ...
Type-based data structure verification
PLDI '09: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe 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 ...
Type-based data structure verification
PLDI '09We 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 ...
Comments