Modular verification of higher-order functional programs

DOI10.1007/978-3-662-54434-1_31MaRDI QIDQ2988670zbMATH OpenOpenAlexFDO

Authors Ryosuke Sato, Naoki Kobayashi

Publication date 19 May 2017

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-54434-1_31

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automating relatively complete verification of higher-order functional programs
• Model checking higher-order programs
• Verifying higher-order functions with tree automata
• Higher-order model checking in direct style
• Verification of tree-processing programs via higher-order model checking

Cites work

• Automata-based abstraction for automated verification of higher-order tree-processing programs
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Automating relatively complete verification of higher-order functional programs
• Compositional and lightweight dependent type inference for ML
• Dafny: an automatic program verifier for functional correctness
• Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
• Dependent types from counterexamples
• Higher-order model checking in direct style
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• Learning refinement types
• Low-level liquid types
• Refinement types for Haskell
• Soft contract verification
• Verifying higher-order functional programs with pattern-matching algebraic data types
• Why3 -- where programs meet provers

Cited in

(15)

• Modular correctness proofs of behavioural implementations
• Sound and complete concolic testing for higher-order functions
• Higher-order program verification via HFL model checking
• Executing and verifying higher-order functional-imperative programs in Maude
• Compositional and lightweight dependent type inference for ML
• Automating relatively complete verification of higher-order functional programs
• Automata-based abstraction for automated verification of higher-order tree-processing programs
• The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification
• scientific article; zbMATH DE number 1487634 (Why is no real title available?)
• Higher order symbolic execution for contract verification and refutation
• Context-Sensitive Multivariant Assertion Checking in Modular Programs
• Automatic Termination Verification for Higher-Order Functional Programs
• Modular inference of subprogram contracts for safety checking
• Specifying and verifying higher-order Rust iterators
• Symbolic execution game semantics

Describes a project that uses

Uses Software

• Dafny
• Haskell
• Why3
• WhyML
• MoCHi
• LiquidHaskell

This page was built for publication: Modular verification of higher-order functional programs

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