Higher order symbolic execution for contract verification and refutation

DOI10.1017/S0956796816000216MaRDI QIDQ5371996zbMATH OpenOpenAlexFDO

Authors Phúc C. Nguyen, Sam Tobin-Hochstadt, David van Horn

Publication date 23 October 2017

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1507.04817

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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. Our approach is sound and relatively complete with respect to a first-order solver for base type values. Therefore, it can form the basis of automated verification and bug-finding tools for higher-order programs. 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. Our system uses higher-order symbolic execution, leveraging contracts as a source of symbolic values including unknown behavioral values, and employs an updatable heap of contract invariants to reason about flow-sensitive facts. Whenever a contract is refuted, it reports a concrete counterexample reproducing the error, which may involve solving for an unknown function. The 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 an off-the-shelf solver to decide problems without heavy encodings. The approach is competitive with a wide range of existing tools---including type systems, flow analyzers, and model checkers---on their own benchmarks. We have built a tool which analyzes programs written in Racket, and report on its effectiveness in verifying and refuting contracts.

Recommendations

• Soft contract verification
• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
• Symbolic execution proofs for higher order store programs
• Static contract checking for Haskell
• Modular verification of higher-order functional programs

Cites work

• Abstract refinement types
• Abstracting abstract machines
• Compositional and lightweight dependent type inference for ML
• Contracts for higher-order functions
• Contracts made manifest
• Correct blame for contracts, no more scapegoating
• Dependent types from counterexamples
• Dynamic typing: Syntax and proof theory
• HALO, Haskell to logic through denotational semantics
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• scientific article; zbMATH DE number 108549 (Why is no real title available?)
• Model-checking higher-order programs with recursive types
• Modular set-based analysis from contracts
• Nested refinements: a logic for duck typing
• Refinement types for Haskell
• Scalable error detection using Boolean satisfiability
• Soft contract verification
• Static contract checking for Haskell
• Static contract checking with abstract interpretation
• Systematic abstraction of abstract machines
• Temporal higher-order contracts
• Types and higher-order recursion schemes for verification of higher-order programs
• Untyped Recursion Schemes and Infinite Intersection Types
• Verifying higher-order functional programs with pattern-matching algebraic data types

Cited in

(4)

• Sound and complete concolic testing for higher-order functions
• Symbolic abstract contract synthesis in a rewriting framework
• A Debugger-Cooperative Higher-Order Contract System in Python
• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework

Describes a project that uses

Uses Software

• Eiffel
• CVC4

This page was built for publication: Higher order symbolic execution for contract verification and refutation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5371996)