Higher order symbolic execution for contract verification and refutation

DOI10.1017/S0956796816000216zbMath1418.68061arXiv1507.04817OpenAlexW2963827670MaRDI QIDQ5371996

Sam Tobin-Hochstadt, Phúc C. Nguyen, David A. Vanhorn

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)

Related Items (1)

Sound and complete concolic testing for higher-order functions

Uses Software

• Eiffel
• CVC4

Cites Work

• Unnamed Item
• Dynamic typing: Syntax and proof theory
• Soft contract verification
• Refinement types for Haskell
• Compositional and Lightweight Dependent Type Inference for ML
• HALO
• Nested refinements
• Contracts for higher-order functions
• Static Contract Checking with Abstract Interpretation
• Systematic abstraction of abstract machines
• Untyped Recursion Schemes and Infinite Intersection Types
• Abstracting abstract machines
• Temporal higher-order contracts
• Dependent types from counterexamples
• Contracts made manifest
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• Static contract checking for Haskell
• Types and higher-order recursion schemes for verification of higher-order programs
• Scalable error detection using boolean satisfiability
• Abstract Refinement Types
• Model-Checking Higher-Order Programs with Recursive Types
• Modular set-based analysis from contracts
• Correct blame for contracts
• Verifying higher-order functional programs with pattern-matching algebraic data types

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