CFML

swMATH13287MaRDI QIDQ25202

No author found.

Described by source

• Program verification through characteristic formulae

Related Items (6)

Symbolic execution proofs for higher order store programs ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation ⋮ Proof-producing synthesis of ML from higher-order logic ⋮ Characteristic formulae for the verification of imperative programs ⋮ Proof-producing translation of higher-order logic into pure and stateful ML

This page was built for software: CFML