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
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
• Proof-producing synthesis of ML from higher-order logic
• Proof-producing translation of higher-order logic into pure and stateful ML

This page was built for software: CFML