{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:23Z","timestamp":1776891443139,"version":"3.51.2"},"reference-count":64,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2016,12,21]],"date-time":"2016-12-21T00:00:00Z","timestamp":1482278400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We present a new approach to automated reasoning about higher-order programs by endowing symbolic execution with a notion of higher-order, symbolic values. To validate our approach, we use it to develop and evaluate a system for verifying and refuting behavioral software contracts of components in a functional language, which we call\n                    <jats:italic>soft contract verification<\/jats:italic>\n                    . In doing so, we discover a mutually beneficial relation between behavioral contracts and higher-order symbolic execution. Contracts aid symbolic execution by providing a rich language of specifications serving as a basis of symbolic higher-order values; the theory of blame enables modular verification and leads to the theorem that\n                    <jats:italic>verified components can't be blamed<\/jats:italic>\n                    ; and the run-time monitoring of contracts enables\n                    <jats:italic>soft<\/jats:italic>\n                    verification whereby verified and unverified components can safely interact. Conversely, symbolic execution aids contracts by providing compile-time verification and automated test case generation from counter-examples to verification. This relation between symbolic exuection and contracts engenders a virtuous cycle encouraging the gradual use of contracts.\n                  <\/jats:p>\n                  <jats:p>Our approach is able to analyze first-class contracts, recursive data structures, unknown functions, and control-flow-sensitive refinements of values, which are all idiomatic in dynamic languages. It makes effective use of off-the-shelf solvers to decide problems without heavy encodings. Counterexample search is sound and relatively complete with respect to a first-order solver for base type values and counter-examples are reported as concrete values, including functions. Therefore, it can form the basis of automated verification and bug-finding tools for higher-order programs. The approach is competitive with a range of existing tools\u2014including type systems, flow analyzers, and model checkers\u2014on their own benchmarks. We have built a prototype to analyze programs written in Racket and report on its effectiveness in verifying and refuting contracts.<\/jats:p>","DOI":"10.1017\/s0956796816000216","type":"journal-article","created":{"date-parts":[[2016,12,21]],"date-time":"2016-12-21T04:31:37Z","timestamp":1482294697000},"source":"Crossref","is-referenced-by-count":7,"title":["Higher order symbolic execution for contract verification and refutation"],"prefix":"10.46298","volume":"27","author":[{"given":"PH\u00daC C.","family":"NGUY\u00caN","sequence":"first","affiliation":[]},{"given":"SAM","family":"TOBIN-HOCHSTADT","sequence":"additional","affiliation":[]},{"given":"DAVID","family":"VAN HORN","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2016,12,21]]},"reference":[{"key":"S0956796816000216_ref57","doi-asserted-by":"crossref","unstructured":"Vazou N. , Seidel E. L. , Jhala R. , Vytiniotis D. & Jones S. P. (2014, August) Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 269\u2013282.","DOI":"10.1145\/2692915.2628161"},{"key":"S0956796816000216_ref26","doi-asserted-by":"crossref","unstructured":"Johnson J. I. & Van Horn D. (2014, October) Abstracting abstract control. In Proceedings of the 10th ACM Symposium on Dynamic Languages. ACM, pp. 11\u201322.","DOI":"10.1145\/2775052.2661098"},{"key":"S0956796816000216_ref59","doi-asserted-by":"publisher","DOI":"10.1145\/239912.239917"},{"key":"S0956796816000216_ref15","doi-asserted-by":"crossref","unstructured":"Findler R. B. & Felleisen M. (2002, September) Contracts for higher-order functions. In ICFP '02: Proceedings of the seventh ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 48\u201359.","DOI":"10.1145\/581478.581484"},{"key":"S0956796816000216_ref55","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000238"},{"key":"S0956796816000216_ref41","doi-asserted-by":"crossref","unstructured":"Ong C. H. L. (2006) On Model-Checking trees generated by Higher-Order recursion schemes. In 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06). IEEE, pp. 81\u201390.","DOI":"10.1109\/LICS.2006.38"},{"key":"S0956796816000216_ref40","doi-asserted-by":"crossref","unstructured":"Nguy\u00ean P. C. & Van Horn D. (2015) Relatively complete counterexamples for higher-order programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 446\u2013456.","DOI":"10.1145\/2737924.2737971"},{"key":"S0956796816000216_ref13","doi-asserted-by":"crossref","unstructured":"Disney T. , Flanagan C. & McCarthy J. (2011, September) Temporal higher-order contracts. In ICFP '11 Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 176\u2013188.","DOI":"10.1145\/2034773.2034800"},{"key":"S0956796816000216_ref63","unstructured":"Yang J. , Twohey P. , Engler D. & Musuvathi M. (2004) Using model checking to find serious file system errors. In Proceedings of the 6th Symposium on Operating Systems Design and Implementation. USENIX, pp. 273\u2013287."},{"key":"S0956796816000216_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"S0956796816000216_ref25","unstructured":"Hickey R. , Fogus M. & contributors (2013, July). core.contracts."},{"key":"S0956796816000216_ref49","doi-asserted-by":"crossref","unstructured":"Terauchi T. (2010) Dependent types from counterexamples. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 119\u2013130.","DOI":"10.1145\/1706299.1706315"},{"key":"S0956796816000216_ref11","doi-asserted-by":"crossref","unstructured":"Dimoulas C. , Findler R. B. , Flanagan C. & Felleisen M. (2011, January) Correct blame for contracts: No more scapegoating. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 215\u2013226.","DOI":"10.1145\/1926385.1926410"},{"key":"S0956796816000216_ref60","doi-asserted-by":"crossref","unstructured":"Xie Y. & Aiken A. (2005, January) Scalable error detection using boolean satisfiability. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 351\u2013363.","DOI":"10.1145\/1047659.1040334"},{"key":"S0956796816000216_ref8","doi-asserted-by":"crossref","unstructured":"Chugh R. , Herman D. & Jhala R. (2012a, October) Dependent types for JavaScript. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications. ACM, pp. 587\u2013606.","DOI":"10.1145\/2384616.2384659"},{"key":"S0956796816000216_ref54","doi-asserted-by":"crossref","unstructured":"Van Horn D. & Might M. (2010, September) Abstracting abstract machines. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 51\u201362.","DOI":"10.1145\/1863543.1863553"},{"key":"S0956796816000216_ref30","doi-asserted-by":"crossref","unstructured":"Kobayashi N. (2009a) Model-checking higher-order functions. In Proceedings of the 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. ACM, pp. 25\u201336.","DOI":"10.1145\/1599410.1599415"},{"key":"S0956796816000216_ref61","unstructured":"Xu D. N. (2012) Hybrid contract checking via symbolic simplification. In Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation. ACM, pp. 107\u2013116."},{"key":"S0956796816000216_ref4","unstructured":"Cadar C. , Dunbar D. & Engler D. (2008) KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. USENIX Association, pp. 209\u2013224."},{"key":"S0956796816000216_ref14","unstructured":"F\u00e4hndrich M. & Logozzo F. (2011) Static contract checking with abstract interpretation. In Proceedings of the 2010 International Conference on Formal Verification of Object-Oriented Software. Springer, pp. 10\u201330."},{"key":"S0956796816000216_ref56","first-page":"209","volume-title":"European Symposium on Programming","author":"Vazou","year":"2013"},{"key":"S0956796816000216_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"S0956796816000216_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"S0956796816000216_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"S0956796816000216_ref22","doi-asserted-by":"crossref","unstructured":"Greenberg M. , Pierce B. C. & Weirich S. (2010) Contracts made manifest. In POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 353\u2013364.","DOI":"10.1145\/1706299.1706341"},{"key":"S0956796816000216_ref36","doi-asserted-by":"crossref","unstructured":"Meunier P. , Findler R. B. & Felleisen M. (2006, January) Modular set-based analysis from contracts. In POPL '06: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 218\u2013231.","DOI":"10.1145\/1111037.1111057"},{"key":"S0956796816000216_ref1","doi-asserted-by":"crossref","unstructured":"Aiken A. , Wimmers E. L. & Lakshman T. K. (1994) Soft typing with conditional types. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM - New York, New York, USA, pp. 163\u2013173.","DOI":"10.1145\/174675.177847"},{"key":"S0956796816000216_ref32","first-page":"431","volume-title":"European Symposium on Programming","author":"Kobayashi","year":"2013"},{"key":"S0956796816000216_ref9","doi-asserted-by":"crossref","unstructured":"Chugh R. , Rondon P. M. & Jhala R. (2012b, January) Nested refinements: A logic for duck typing. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 231\u2013244.","DOI":"10.1145\/2103656.2103686"},{"key":"S0956796816000216_ref33","doi-asserted-by":"crossref","unstructured":"Kobayashi N. & Ong C. H. L. (2009, August) A type system equivalent to the modal Mu-Calculus model checking of Higher-Order recursion schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic In Computer Science. IEEE, pp. 179\u2013188.","DOI":"10.1109\/LICS.2009.29"},{"key":"S0956796816000216_ref39","doi-asserted-by":"crossref","unstructured":"Nguy\u00ean P. C. , Tobin-Hochstadt S. & Van Horn D. (2014) Soft contract verification. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 139\u2013152.","DOI":"10.1145\/2628136.2628156"},{"key":"S0956796816000216_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/316686.316703"},{"key":"S0956796816000216_ref18","unstructured":"Flatt M. & PLT (2010) Reference: Racket. Technical Report PLT-TR-2010-1, PLT Inc."},{"key":"S0956796816000216_ref58","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"},{"key":"S0956796816000216_ref34","doi-asserted-by":"crossref","unstructured":"Kobayashi N. , Sato R. & Unno H. (2011, June) Predicate abstraction and CEGAR for higher-order model checking. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 222\u2013233.","DOI":"10.1145\/1993498.1993525"},{"key":"S0956796816000216_ref10","doi-asserted-by":"crossref","unstructured":"Claessen K. & Hughes J. (2000) QuickCheck: A lightweight tool for random testing of Haskell programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 268\u2013279.","DOI":"10.1145\/351240.351266"},{"key":"S0956796816000216_ref53","unstructured":"Tsukada T. & Kobayashi N. (2010) Untyped recursion schemes and infinite intersection types. In Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures. Springer-Verlag, pp. 343\u2013357."},{"key":"S0956796816000216_ref19","doi-asserted-by":"crossref","unstructured":"Foster J. S. , Terauchi T. & Aiken A. (2002, May) Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 1\u201312.","DOI":"10.1145\/543552.512531"},{"key":"S0956796816000216_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13953-6_9"},{"key":"S0956796816000216_ref35","doi-asserted-by":"crossref","unstructured":"Kobayashi N. , Tabuchi N. & Unno H. (2010, January) Higher-order multi-parameter tree transducers and recursion schemes for program verification. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 495\u2013508.","DOI":"10.1145\/1706299.1706355"},{"key":"S0956796816000216_ref38","unstructured":"Moura L. D. & Bj\u00f8rner N. (2008) Z3: An efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, pp. 337\u2013340."},{"key":"S0956796816000216_ref20","doi-asserted-by":"crossref","unstructured":"Freeman T. & Pfenning F. (1991, June) Refinement types for ML. In Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation. ACM, pp. 268\u2013277.","DOI":"10.1145\/113446.113468"},{"key":"S0956796816000216_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27694-1_21"},{"key":"S0956796816000216_ref2","doi-asserted-by":"crossref","unstructured":"Austin T. H. , Disney T. & Flanagan C. (2011, October) Virtual values for language extension. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications. ACM, pp. 921\u2013938.","DOI":"10.1145\/2048066.2048136"},{"key":"S0956796816000216_ref50","doi-asserted-by":"crossref","unstructured":"Tobin-Hochstadt S. & Felleisen M. (2010, September) Logical types for untyped languages. In ICFP '10: International Conference on Functional Programming. ACM, pp. 117\u2013128.","DOI":"10.1145\/1863543.1863561"},{"key":"S0956796816000216_ref46","doi-asserted-by":"crossref","unstructured":"Shivers O. (1988) Control flow analysis in Scheme. In PLDI '88: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation. ACM, pp. 164\u2013174.","DOI":"10.1145\/53990.54007"},{"key":"S0956796816000216_ref21","doi-asserted-by":"crossref","unstructured":"Godefroid P. , Klarlund N. & Sen K. (2005, June) DART: Directed automated random testing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 213\u2013223.","DOI":"10.1145\/1065010.1065036"},{"key":"S0956796816000216_ref48","doi-asserted-by":"crossref","unstructured":"Strickland T. S. , Tobin-Hochstadt S. , Findler R. B. & Flatt M. (2012, October) Chaperones and impersonators: Run-time support for reasonable interposition. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications. ACM, pp. 943\u2013962.","DOI":"10.1145\/2398857.2384685"},{"key":"S0956796816000216_ref31","doi-asserted-by":"crossref","unstructured":"Kobayashi N. (2009b, January) Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 416\u2013428.","DOI":"10.1145\/1480881.1480933"},{"key":"S0956796816000216_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234747"},{"key":"S0956796816000216_ref6","doi-asserted-by":"crossref","unstructured":"Cartwright R. & Fagan M. (1991) Soft typing. In Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation. ACM, pp. 278\u2013292.","DOI":"10.1145\/113445.113469"},{"key":"S0956796816000216_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384655"},{"key":"S0956796816000216_ref51","doi-asserted-by":"crossref","unstructured":"Tobin-Hochstadt S. , St-Amour V. , Culpepper R. , Flatt M. & Felleisen M. (2011, June) Languages as libraries. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 132\u2013141.","DOI":"10.1145\/1993498.1993514"},{"key":"S0956796816000216_ref42","doi-asserted-by":"crossref","unstructured":"Ong C. H. L. & Ramsay S. J. (2011, January) Verifying higher-order functional programs with pattern-matching algebraic data types. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 587\u2013598.","DOI":"10.1145\/1926385.1926453"},{"key":"S0956796816000216_ref5","doi-asserted-by":"crossref","unstructured":"Cadar C. , Ganesh V. , Pawlowski P. M. , Dill D. L. & Engler D. R. (2006) EXE: Automatically generating inputs of death. In Proceedings of the 13th ACM Conference on Computer and Communications Security. ACM, pp. 322\u2013335.","DOI":"10.1145\/1180405.1180445"},{"key":"S0956796816000216_ref44","doi-asserted-by":"crossref","unstructured":"Rondon P. M. , Kawaguci M. & Jhala R. (2008) Liquid types. In Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 159\u2013169.","DOI":"10.1145\/1375581.1375602"},{"key":"S0956796816000216_ref12","unstructured":"Disney T. (2013, July) contracts.coffee."},{"key":"S0956796816000216_ref64","unstructured":"Zhu H. & Jagannathan S. (2013) Compositional and lightweight dependent type inference for ML. In Conference on Verification, Model-Checking and Abstract Interpretation Springer, 295\u2013314."},{"key":"S0956796816000216_ref62","unstructured":"Xu D. N. , Peyton Jones, S. & Claessen S. (2009) Static contract checking for Haskell. In POPL '09: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 41\u201352."},{"key":"S0956796816000216_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_12"},{"key":"S0956796816000216_ref17","doi-asserted-by":"crossref","unstructured":"Flanagan C. , Flatt M. , Krishnamurthi S. , Weirich S. & Felleisen M. (1996, May) Catching bugs in the web of program invariants. In PLDI '96: Proceedings of the ACM SIGPLAN 1996 Conference on Programming Language Design and Implementation. ACM, pp. 23\u201332.","DOI":"10.1145\/231379.231387"},{"key":"S0956796816000216_ref43","doi-asserted-by":"crossref","unstructured":"Plosch R. (1997, December) Design by contract for Python. In Proceedings of the Joint Asia Pacific Software Engineering Conference. IEEE, pp. 213\u2013219.","DOI":"10.1109\/APSEC.1997.640178"},{"key":"S0956796816000216_ref28","doi-asserted-by":"crossref","unstructured":"Klein C. , Flatt M. & Findler R. B. (2010) Random testing for higher-order, stateful programs. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications. ACM, pp. 555\u2013566.","DOI":"10.1145\/1869459.1869505"},{"key":"S0956796816000216_ref37","volume-title":"Eiffel: The Language","author":"Meyer","year":"1991"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796816000216","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:53Z","timestamp":1776889193000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796816000216\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,21]]},"references-count":64,"alternative-id":["S0956796816000216"],"URL":"https:\/\/doi.org\/10.1017\/s0956796816000216","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,12,21]]},"article-number":"e3"}}