Higher order symbolic execution for contract verification and refutation*. (21st December 2016)

• Record Type: Journal Article
• Authors: NGUYÊN, PHÚC C.; TOBIN-HOCHSTADT, SAM; VAN HORN, DAVID
• Is Part Of: Journal of functional programming. Volume 27(2017)
• Publication Date: 2016-12-21
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796816000216
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: 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 soft contract verification . 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 verified components can't be blamed ; and the run-time monitoring of contracts enables soft 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. 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—including type systems, flow analyzers, and model checkers—on their own benchmarks. We have built a prototype to analyze programs written in Racket and report on its effectiveness in verifying and refuting contracts.