Higher order symbolic execution for contract verification and refutation
| Autor: | David Van Horn, Sam Tobin-Hochstadt, Phuc C. Nguyen |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Functional programming
Relation (database) Computer science business.industry Programming language 020207 software engineering 02 engineering and technology Modular design Solver Symbolic execution Data structure computer.software_genre 020204 information systems 0202 electrical engineering electronic engineering information engineering Automated reasoning business computer Software Counterexample |
| Zdroj: | Journal of Functional Programming. 27 |
| ISSN: | 1469-7653 0956-7968 |
| DOI: | 10.1017/s0956796816000216 |
| Popis: | 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 callsoft 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 thatverified components can't be blamed; and the run-time monitoring of contracts enablessoftverification 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|