Verified characteristic formulae for CakeML

DOI10.1007/978-3-662-54434-1_22MaRDI QIDQ2988660zbMATH OpenOpenAlexFDO

Authors Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish

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_22

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)

Recommendations

• Characteristic formulae for the verification of imperative programs
• Program verification through characteristic formulae
• CakeML
• The verified CakeML compiler backend
• A verified compiler from Isabelle/HOL to CakeML

Cites work

• CakeML
• Characteristic formulae for the verification of imperative programs
• Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
• Effective interactive proofs for higher-order imperative programs
• Fiat: deductive synthesis of abstract data types in a proof assistant
• HALO
• HALO, Haskell to logic through denotational semantics
• Logic for Programming, Artificial Intelligence, and Reasoning
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
• Program verification through characteristic formulae
• Proof-producing translation of higher-order logic into pure and stateful ML
• Refinement through restraint: bringing down the cost of verification
• Refinement to Imperative/HOL
• Self-certification: bootstrapping certified typecheckers in F^ with Coq
• The HOL-Omega Logic
• The verified CakeML compiler backend
• Verified software toolchain (invited talk)

Cited in

(12)

• Proof-producing synthesis of CakeML from monadic HOL functions
• Connecting higher-order separation logic to a first-order outside world
• CakeML
• A verified proof checker for higher-order logic
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• A mechanised semantics for HOL with ad-hoc overloading
• Certified MaxSAT preprocessing
• Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
• The verified CakeML compiler backend
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

Describes a project that uses

Uses Software

• Bedrock
• HALO
• CertiCoq
• Fiat
• seL4
• Toolchain
• CakeML
• HOL-Omega
• OCaml
• Haskell
• Coq

This page was built for publication: Verified characteristic formulae for CakeML

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