Sam Tobin-Hochstadt
ABSTRACT
We present a new approach to automated reasoning about higher-order programs by extending symbolic execution to use behavioral contracts as symbolic values, thus enabling symbolic approximation of higher-order behavior.
Our approach is based on the idea of an abstract reduction semantics that gives an operational semantics to programs with both concrete and symbolic components. Symbolic components are approximated by their contract and our semantics gives an operational interpretation of contracts-as-values. The result is an executable semantics that soundly predicts program behavior, including contract failures, for all possible instantiations of symbolic components. We show that our approach scales to an expressive language of contracts including arbitrary programs embedded as predicates, dependent function contracts, and recursive contracts. Supporting this rich language of specifications leads to powerful symbolic reasoning using existing program constructs.
We then apply our approach to produce a verifier for contract correctness of components, including a sound and computable approximation to our semantics that facilitates fully automated contract verification. Our implementation is capable of verifying contracts expressed in existing programs, and of justifying contract-elimination optimizations.
Supplemental Material
Available for Download
zip
res0162.zip (62.5 KB)
This appendix presents the full definitions of the type systems, metafunctions, and relations from the main content of the paper.
- J. Michael Ashley and R. Kent Dybvig. A practical and flexible flow analysis for higher-order languages. ACM Trans. on Program. Lang. Syst., 20 (4): 845--868, 1998. Google Scholar
Digital Library
- Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. Automatic predicate abstraction of C programs. In Proceedings of the Conference on Programming Language Design and Implementation, pages 203--213, 2001. Google ScholarDigital Library
- Thomas Ball, Vladimir Levin, and Sriram K. Rajamani. A decade of software model checking with SLAM. Commun. ACM, 54 (7): 68--76, 2011. Google ScholarDigital Library
- Anindya Banerjee. A modular, polyvariant and type-based closure analysis. In Proceedings of the International Conference on Functional Programming, pages 1--10, 1997. Google ScholarDigital Library
- Anindya Banerjee and Thomas Jensen. Modular control-flow analysis with rank 2 intersection types. Mathematical. Structures in Comp. Sci., 13 (1): 87--124, 2003. Google ScholarDigital Library
- M. Barnett, M. Fähndrich, K. R. M. Leino, P. Müller, W. Schulte, and H. Venter. Specification and verification: The Spec# experience. Commun. ACM, 54 (6): 81--91, 2010. Google ScholarDigital Library
- Matthias Blume and David McAllester. Sound and complete models of contracts. J. Funct. Program., 16 (4--5): 375--414, 2006. Google ScholarDigital Library
- Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. EXE: automatically generating inputs of death. In Proceedings of the Conference on Computer and Communications Security, pages 322--335, 2006. Google ScholarDigital Library
- Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the Conference on Operating Systems Design and Implementation, pages 209--224, 2008. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Symposium on Principles of Programming Languages, pages 238--252, 1977. Google ScholarDigital Library
- P. L. Curien. An abstract framework for environment machines. Theoretical Computer Science, 82 (2): 389--402, 1991. Google ScholarDigital Library
- Christos Dimoulas and Matthias Felleisen. On contract satisfaction in a higher-order world. ACM Trans. on Program. Lang. Syst., 33, 2011. Google ScholarDigital Library
- Christos Dimoulas, Robert B. Findler, Cormac Flanagan, and Matthias Felleisen. Correct blame for contracts: no more scapegoating. In Proceedings of the Symposium on Principles of Programming Languages, pages 215--226, 2011. Google ScholarDigital Library
- Manuel Fähndrich and Francesco Logozzo. Static contract checking with abstract interpretation. In Proceedings of the 2010 International Conference on Formal Verification of Object-Oriented Software, pages 10--30, 2011. Google ScholarDigital Library
- Manuel Fähndrich, Michael Barnett, and Francesco Logozzo. Embedded contract languages. In Proceedings of the Symposium on Applied Computing, pages 2103--2110, 2010. Google ScholarDigital Library
- Matthias Felleisen, Robert B. Findler, Matthew Flatt, and Shriram Krishnamurthi. How to design programs: an introduction to programming and computing. MIT Press, 2001. Google ScholarDigital Library
- Robert B. Findler and Matthias Felleisen. Contracts for higher-order functions. In ICFP '02: Proceedings of the seventh ACM SIGPLAN International Conference on Functional Programming, pages 48--59, 2002. Google ScholarDigital Library
- Cormac Flanagan. Effective Static Debugging via Componential Set-Based Analysis. PhD thesis, Rice University, 1997.Google Scholar
- Matthew Flatt and PLT. Reference: Racket. Technical Report PLT-TR-2010--1, PLT Inc., 2010.Google Scholar
- Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: directed automated random testing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 213--223. ACM, 2005. Google ScholarDigital Library
- M. Greenberg. personal communication.Google Scholar
- Ralf Hinze, Johan Jeuring, and Andres Löh. Typed contracts for functional programming. In Functional and Logic Programming, volume 3945 of LNCS, chapter 15, pages 208--225. 2006. Google ScholarDigital Library
- Ralph Johan, Abo Akademi, and J. Von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag New York, Inc., 1998. Google ScholarDigital Library
- James C. King. Symbolic execution and program testing. Commun. ACM, 19 (7): 385--394, 1976. Google ScholarDigital Library
- Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of the Symposium on Principles of Programming Languages, pages 416--428, 2009. Google ScholarDigital Library
- Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. Predicate abstraction and CEGAR for higher-order model checking. In Proceedings of the Conference on Programming Language Design and Implementation, pages 222--233, 2011. Google ScholarDigital Library
- George Kuan, David MacQueen, and Robert B. Findler. A rewriting semantics for type inference. In Proceedings of the European Symposium on Programming, volume 4421, 2007. Google ScholarDigital Library
- Oukseh Lee, Kwangkeun Yi, and Yunheung Paek. A proof method for the correctness of modularized 0CFA. Info. Proc. Letters, 81: 179--185, 2002. Google ScholarDigital Library
- Philippe Meunier. Modular Set-Based Analysis from Contracts. PhD thesis, Northeastern University, 2006.Google Scholar
- Philippe Meunier, Robert B. Findler, and Matthias Felleisen. Modular set-based analysis from contracts. In POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 218--231, 2006. Google ScholarDigital Library
- Bertrand Meyer. Eiffel : The Language. Prentice Hall, 1991. Google ScholarDigital Library
- Matthew Might and Olin Shivers. Improving flow analyses via(Γ)CFA: Abstract garbage collection and counting. In Proceedings of the International Conference on Functional Programming, pages 13--25, 2006. Google ScholarDigital Library
- G. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5 (3): 223--255, 1977.Google ScholarCross Ref
- John Reppy. Type-sensitive control-flow analysis. In ML '06: Proceedings of the 2006 Workshop on ML, pages 74--83, 2006. Google ScholarDigital Library
- Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. Liquid types. In Programming Languages Design and Implementation, PLDI '08, pages 159--169. ACM, 2008. Google ScholarDigital Library
- Koushik Sen, Darko Marinov, and Gul Agha. CUTE: a concolic unit testing engine for C. SIGSOFT Softw. Eng. Notes, 30 (5): 263--272, 2005. Google ScholarDigital Library
- Manuel Serrano. Control flow analysis: a functional languages compilation paradigm. In Proceedings of the Symposium on Applied Computing, pages 118--122, 1995. Google ScholarDigital Library
- Olin Shivers. Control-flow analysis of higher-order languages. PhD thesis, Carnegie Mellon University, 1991. Google ScholarDigital Library
- T. Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt. Chaperones and impersonators: Runtime support for reasonable interposition. In OOPSLA '12: Object-Oriented Programming, Systems, Languages, and Applications, 2012. Google ScholarDigital Library
- Peter Thiemann. Higher-Order redundancy elimination. In Proceedings of the Workshop on Partial Evaluation and Program Manipulation, pages 73--84, 1994.Google Scholar
- Sam Tobin-Hochstadt and Matthias Felleisen. Logical types for untyped languages. In Proceedings of the International Conference on Functional Programming, pages 117--128, 2010. Google ScholarDigital Library
- David Van Horn and Matthew Might. Abstracting abstract machines. In Proceedings of the International Conference on Functional Programming, pages 51--62, 2010. Google ScholarDigital Library
- Dana N. Xu. Hybrid contract checking via symbolic simplification. In Proceedings of the Workshop on Partial Evaluation and Program Manipulation, pages 107--116, 2012. Google ScholarDigital Library
- Dana N. Xu, Simon Peyton Jones, and Simon Claessen. Static contract checking for Haskell. In POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 41--52, 2009. Google ScholarDigital Library
Index Terms
- Higher-order symbolic execution via contracts
Recommendations
Higher-order symbolic execution via contracts
OOPSLA '12We present a new approach to automated reasoning about higher-order programs by extending symbolic execution to use behavioral contracts as symbolic values, thus enabling symbolic approximation of higher-order behavior.
Our approach is based on the idea ...
Blame assignment for higher-order contracts with intersection and union
ICFP '15We present an untyped calculus of blame assignment for a higher-order contract system with two new operators: intersection and union. The specification of these operators is based on the corresponding type theoretic constructions. This connection makes ...
Blame assignment for higher-order contracts with intersection and union
ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional ProgrammingWe present an untyped calculus of blame assignment for a higher-order contract system with two new operators: intersection and union. The specification of these operators is based on the corresponding type theoretic constructions. This connection makes ...
Comments