CFML

swMATH13287MaRDI QIDQ25202FDOQ25202

Author name not available (Why is that?)

Described by source

• Program verification through characteristic formulae

Cited In (6)

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

This page was built for software: CFML