Dana N. Xu
ABSTRACT
Program errors are hard to detect or prove absent. Allowing programmers to write formal and precise specifications, especially in the form of contracts, is a popular approach to program verification and error discovery. We formalize and implement a hybrid (static and dynamic) contract checker for a subset of OCaml. The key technique is symbolic simplification, which makes integrating static and dynamic contract checking easy and effective. Our technique statically checks contract satisfaction or blames the function violating the contract. When a contract satisfaction is undecidable, it leaves residual code for dynamic contract checking.
- N. Ayache and J.-C. Filliatre. Combining the Coq proof assistant with first-order decision procedures. Unpublished, 2006. URL http://www.lri.fr/ filliatr/publis/coq-dp.ps.Google Scholar
- M. Barnett, K. R. M. Leino, and W. Schulte. The Spec\# programming system: An overview. CASSIS, LNCS 3362, 2004. Google ScholarDigital Library
- J. F. Belo, M. Greenberg, A. Igarashi, and B. C. Pierce. Polymorphic contracts. In ESOP, pages 18--37, 2011. Google ScholarDigital Library
- A. M. Ben-Amram and C. S. Lee. Program termination analysis in polynomial time. ACM Trans. Program. Lang. Syst., 29: 5:1--5:37, January 2007. Google ScholarDigital Library
- J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. ACM Trans. Program. Lang. Syst., 33: 8:1--8:45, February 2011. Google ScholarDigital Library
- e, and Paulson}Sledgehammer:CADE11J. C. Blanchette, S. Böhme, and L. C. Paulson. Extending Sledgehammer with SMT solvers. In CADE, pages 116--130, 2011. Google ScholarDigital Library
- M. Blume and D. A. McAllester. Sound and complete models of contracts. J. Funct. Program., 16 (4--5): 375--414, 2006. Google ScholarDigital Library
- S. Conchon, E. Contejean, and J. Kanig. Ergo : a theorem prover for polymorphic first-order logic modulo theories. Unpublished, 2006. URL http://ergo.lri.fr/papers/ergo.ps.Google Scholar
- J.-F. Couchot and S. Lescuyer. Handling polymorphism in automated deduction. In CADE, pages 263--278, 2007. Google ScholarDigital Library
- M. Fahndrich and F. Logozzo. Static contract checking with abstract interpretation. In FoVeOOS: the Intl. Conf. on Formal Verf. of OO Software, pages 10--30, 2010. Google ScholarDigital Library
- R. B. Findler and M. Blume. Contracts as pairs of projections. In Functional and Logic Prog., pages 226--241, 2006. Google ScholarDigital Library
- R. B. Findler and M. Felleisen. Contracts for higher-order functions. In ICFP: the ACM SIGPLAN Intl. Conf. on Fnl. Prog., pages 48--59, 2002. Google ScholarDigital Library
- C. Flanagan. Hybrid type checking. In POPL: the ACM SIGPLAN-SIGACT symp. on Prin. of Prog. Lang., pages 245--256, 2006. Google ScholarDigital Library
- C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In PLDI: the ACM SIGPLAN conf. on Prog. Lang. Design and Impl., pages 237--247. ACM, 1993. Google ScholarDigital Library
- C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI, pages 234--245, 2002. Google ScholarDigital Library
- M. Greenberg, B. C. Pierce, and S. Weirich. Contracts made manifest. In POPL: the ACM SIGPLAN-SIGACT symp. on Prin. of Prog. Lang., pages 353--364, 2010. Google ScholarDigital Library
- C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12: 576--580, October 1969. Google ScholarDigital Library
- K. Honda and N. Yoshida. A compositional logic for polymorphic higher-order functions. In PPDP: the ACM SIGPLAN intl. conf. on Prin. and practice of Decl. Prog., pages 191--202, 2004. Google ScholarDigital Library
- K. Honda, M. Berger, and N. Yoshida. Descriptive and relative completeness of logics for higher-order functions. In ICALP: the Intl. Colloq. on Autamata, Lang. and Prog., pages 360--371, 2006. Google ScholarDigital Library
- B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In NASA Formal Methods, pages 41--55, 2011. Google ScholarCross Ref
- R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: Verifying functional programs using abstract interpreters. In CAV: the intl. conf. on Comp. Aided Verf., pages 262--274, 2011. Google ScholarDigital Library
- M. Kerber. How to prove higher order theorems in first order logic. In IJCAI, pages 137--142, 1991. Google ScholarDigital Library
- Y. P. Khoo, B.-Y. E. Chang, and J. S. Foster. Mixing type checking and symbolic execution. In PLDI: the ACM SIGPLAN conf. on Prog. Lang. Design and Impl., pages 436--447, 2010. Google ScholarDigital Library
- K. Knowles and C. Flanagan. Hybrid type checking. ACM Trans. Program. Lang. Syst., 32: 6:1--6:34, February 2010. Google ScholarDigital Library
- N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL, pages 416--428, 2009. Google ScholarDigital Library
- N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and cegar for higher-order model checking. In PLDI, pages 222--233, 2011. Google ScholarDigital Library
- C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In POPL, pages 81--92, 2001. Google ScholarDigital Library
- K. R. M. Leino and P. Rümmer. A polymorphic intermediate verification language: Design and logical encoding. In TACAS: the Intl. Conf. on Tools and Algo. for the Construction and Anls. of Syst., pages 312--327, 2010. Google ScholarDigital Library
- B. Meyer. Eiffel: the language. Prentice-Hall, 1992. Google ScholarDigital Library
- M. Might. Logic-flow analysis of higher-order programs. In POPL: the ACM SIGPLAN-SIGACT symp. on Prin. of Prog. Lang., pages 185--198, 2007. Google ScholarDigital Library
- A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in Hoare type theory. In ICFP, pages 62--73, 2006. Google ScholarDigital Library
- C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS: IEEE Symp. on Logic in Computer Science, pages 81--90, 2006. Google ScholarDigital Library
- C.-H. L. Ong and S. J. Ramsay. Verifying higher-order functional programs with pattern-matching algebraic data types. In POPL, pages 587--598, 2011. Google ScholarDigital Library
- Y. Régis-Gianas and F. Pottier. A Hoare logic for call-by-value functional programs. In MPC, pages 305--335, 2008. Google ScholarDigital Library
- D. Sereni and N. D. Jones. Termination analysis of higher-order functional programs. In proceedings of the 3rd Asian Symp. on Program. Lang. and Systems (APLAS), pages 281--297, 2005. Google ScholarDigital Library
- N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with value-dependent types. In ICFP, pages 15--27, 2011. Google ScholarDigital Library
- H. Xi and F. Pfenning. Dependent types in practical programming. In POPL: the ACM SIGPLAN-SIGACT symp. on Prin. of Prog. Lang., pages 214--227, 1999. Google ScholarDigital Library
- D. N. Xu. Extended static checking for Haskell. In Proceedings of the ACM SIGPLAN workshop on Haskell, pages 48--59, 2006. Google ScholarDigital Library
- D. N. Xu. Hybrid contract checking via symbolic simplification. INRIA technical report RR-7794, 2011.Google Scholar
- D. N. Xu, S. Peyton Jones, and K. Claessen. Static contract checking for Haskell. In POPL, pages 41--52, 2009. Google ScholarDigital Library
- N. Xu. Static Contract Checking for Haskell. Ph.D. thesis, Aug. 2008.Google Scholar
Index Terms
- Hybrid contract checking via symbolic simplification
Recommendations
Static contract checking for Haskell
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesProgram errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and for systems that are guarded by runtime checks. Static verification techniques have been applied to imperative and object-oriented ...
Enhancing spark's contract checking facilities using symbolic execution
Spark, a subset of Ada for engineering safety and security-critical systems, is one of the best commercially available frameworks for formal-methods-supported development of critical software. Spark is designed for verification and includes a software ...
Comments