research-article

Higher-order symbolic execution via contracts

Authors:

Sam Tobin-Hochstadt,

David Van HornAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 10

Pages 537 - 554

https://doi.org/10.1145/2398857.2384655

Published: 19 October 2012 Publication History

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.

Supplementary Material

ZIP File (res0162.zip)

This appendix presents the full definitions of the type systems, metafunctions, and relations from the main content of the paper.

Download
62.50 KB

References

[1]

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.

Digital Library

[2]

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.

Digital Library

[3]

Thomas Ball, Vladimir Levin, and Sriram K. Rajamani. A decade of software model checking with SLAM. Commun. ACM, 54 (7): 68--76, 2011.

Digital Library

[4]

Anindya Banerjee. A modular, polyvariant and type-based closure analysis. In Proceedings of the International Conference on Functional Programming, pages 1--10, 1997.

Digital Library

[5]

Anindya Banerjee and Thomas Jensen. Modular control-flow analysis with rank 2 intersection types. Mathematical. Structures in Comp. Sci., 13 (1): 87--124, 2003.

Digital Library

[6]

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.

Digital Library

[7]

Matthias Blume and David McAllester. Sound and complete models of contracts. J. Funct. Program., 16 (4--5): 375--414, 2006.

Digital Library

[8]

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.

Digital Library

[9]

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.

Digital Library

[10]

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.

Digital Library

[11]

P. L. Curien. An abstract framework for environment machines. Theoretical Computer Science, 82 (2): 389--402, 1991.

Digital Library

[12]

Christos Dimoulas and Matthias Felleisen. On contract satisfaction in a higher-order world. ACM Trans. on Program. Lang. Syst., 33, 2011.

Digital Library

[13]

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.

Digital Library

[14]

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.

Digital Library

[15]

Manuel Fähndrich, Michael Barnett, and Francesco Logozzo. Embedded contract languages. In Proceedings of the Symposium on Applied Computing, pages 2103--2110, 2010.

Digital Library

[16]

Matthias Felleisen, Robert B. Findler, Matthew Flatt, and Shriram Krishnamurthi. How to design programs: an introduction to programming and computing. MIT Press, 2001.

Digital Library

[17]

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.

Digital Library

[18]

Cormac Flanagan. Effective Static Debugging via Componential Set-Based Analysis. PhD thesis, Rice University, 1997.

[19]

Matthew Flatt and PLT. Reference: Racket. Technical Report PLT-TR-2010--1, PLT Inc., 2010.

[20]

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.

Digital Library

[21]

M. Greenberg. personal communication.

[22]

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.

Digital Library

[23]

Ralph Johan, Abo Akademi, and J. Von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag New York, Inc., 1998.

Digital Library

[24]

James C. King. Symbolic execution and program testing. Commun. ACM, 19 (7): 385--394, 1976.

Digital Library

[25]

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.

Digital Library

[26]

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.

Digital Library

[27]

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.

Digital Library

[28]

Oukseh Lee, Kwangkeun Yi, and Yunheung Paek. A proof method for the correctness of modularized 0CFA. Info. Proc. Letters, 81: 179--185, 2002.

Digital Library

[29]

Philippe Meunier. Modular Set-Based Analysis from Contracts. PhD thesis, Northeastern University, 2006.

[30]

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.

Digital Library

[31]

Bertrand Meyer. Eiffel : The Language. Prentice Hall, 1991.

Digital Library

[32]

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.

Digital Library

[33]

G. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5 (3): 223--255, 1977.

[34]

John Reppy. Type-sensitive control-flow analysis. In ML '06: Proceedings of the 2006 Workshop on ML, pages 74--83, 2006.

Digital Library

[35]

Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. Liquid types. In Programming Languages Design and Implementation, PLDI '08, pages 159--169. ACM, 2008.

Digital Library

[36]

Koushik Sen, Darko Marinov, and Gul Agha. CUTE: a concolic unit testing engine for C. SIGSOFT Softw. Eng. Notes, 30 (5): 263--272, 2005.

Digital Library

[37]

Manuel Serrano. Control flow analysis: a functional languages compilation paradigm. In Proceedings of the Symposium on Applied Computing, pages 118--122, 1995.

Digital Library

[38]

Olin Shivers. Control-flow analysis of higher-order languages. PhD thesis, Carnegie Mellon University, 1991.

Digital Library

[39]

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.

Digital Library

[40]

Peter Thiemann. Higher-Order redundancy elimination. In Proceedings of the Workshop on Partial Evaluation and Program Manipulation, pages 73--84, 1994.

[41]

Sam Tobin-Hochstadt and Matthias Felleisen. Logical types for untyped languages. In Proceedings of the International Conference on Functional Programming, pages 117--128, 2010.

Digital Library

[42]

David Van Horn and Matthew Might. Abstracting abstract machines. In Proceedings of the International Conference on Functional Programming, pages 51--62, 2010.

Digital Library

[43]

Dana N. Xu. Hybrid contract checking via symbolic simplification. In Proceedings of the Workshop on Partial Evaluation and Program Manipulation, pages 107--116, 2012.

Digital Library

[44]

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.

Digital Library

Cited By

You SFindler RDimoulas C(2021)Sound and Complete Concolic Testing for Higher-order FunctionsProgramming Languages and Systems10.1007/978-3-030-72019-3_23(635-663)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_23
Hallahan WXue ABland MJhala RPiskac RMcKinley KFisher K(2019)Lazy counterfactual symbolic executionProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314618(411-424)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314618
Greenberg M(2019)Space-Efficient Latent ContractsTrends in Functional Programming10.1007/978-3-030-14805-8_1(3-23)Online publication date: 21-Feb-2019
https://doi.org/10.1007/978-3-030-14805-8_1
Show More Cited By

Index Terms

Higher-order symbolic execution via contracts

Recommendations

Higher-order symbolic execution via contracts
OOPSLA '12: Proceedings of the ACM international conference on Object oriented programming systems languages and applications

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 ...
Blame assignment for higher-order contracts with intersection and union
ICFP '15

We 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 Programming

We 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 47, Issue 10

OOPSLA '12

October 2012

1011 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2398857

Issue’s Table of Contents

OOPSLA '12: Proceedings of the ACM international conference on Object oriented programming systems languages and applications
October 2012
1052 pages
ISBN:9781450315616
DOI:10.1145/2384616
General Chair:
Gary T. Leavens
University of Central Florida
,
Program Chair:
Matthew B. Dwyer
University of Nebraska - Lincoln

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 October 2012

Published in SIGPLAN Volume 47, Issue 10

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

52
Total Citations
View Citations
451
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)3

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

You SFindler RDimoulas C(2021)Sound and Complete Concolic Testing for Higher-order FunctionsProgramming Languages and Systems10.1007/978-3-030-72019-3_23(635-663)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_23
Hallahan WXue ABland MJhala RPiskac RMcKinley KFisher K(2019)Lazy counterfactual symbolic executionProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314618(411-424)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314618
Greenberg M(2019)Space-Efficient Latent ContractsTrends in Functional Programming10.1007/978-3-030-14805-8_1(3-23)Online publication date: 21-Feb-2019
https://doi.org/10.1007/978-3-030-14805-8_1
Vazou NTanter ÉVan Horn D(2018)Gradual liquid type inferenceProceedings of the ACM on Programming Languages10.1145/32765022:OOPSLA(1-25)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276502
Rhodes DDisney TFlanagan C(2014)Dynamic detection of object capability violations through model checkingACM SIGPLAN Notices10.1145/2775052.266109950:2(103-112)Online publication date: 14-Oct-2014
https://dl.acm.org/doi/10.1145/2775052.2661099
Rhodes DDisney TFlanagan CBlack ATratt L(2014)Dynamic detection of object capability violations through model checkingProceedings of the 10th ACM Symposium on Dynamic languages10.1145/2661088.2661099(103-112)Online publication date: 20-Oct-2014
https://dl.acm.org/doi/10.1145/2661088.2661099
Vandenbogaerde BStievenart QDe Roover C(2022)Summary-Based Compositional Analysis for Soft Contract Verification2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation (SCAM)10.1109/SCAM55253.2022.00028(186-196)Online publication date: Oct-2022
https://doi.org/10.1109/SCAM55253.2022.00028
Palmer ZPark TSmith SWeng S(2020)Higher-order demand-driven symbolic evaluationProceedings of the ACM on Programming Languages10.1145/34089844:ICFP(1-28)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408984
Song DLee MOh H(2019)Automatic and scalable detection of logical errors in functional programming assignmentsProceedings of the ACM on Programming Languages10.1145/33606143:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360614
Nguyễn PGilray TTobin-Hochstadt SVan Horn DMcKinley KFisher K(2019)Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programsProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314643(845-859)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314643
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents