Characteristic formulae for liveness properties of non-terminating CakeML programs
From MaRDI portal
Cites work
- scientific article; zbMATH DE number 1670750 (Why is no real title available?)
- scientific article; zbMATH DE number 1693527 (Why is no real title available?)
- scientific article; zbMATH DE number 3688686 (Why is no real title available?)
- A Hoare logic for the coinductive trace-based big-step semantics of While
- A dynamic logic with traces and coinduction
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
- A formally verified compiler back-end
- Characteristic formulae for the verification of imperative programs
- Coinductive big-step operational semantics
- Flag-based big-step semantics
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Non-standard semantics for program slicing
- On the bisimulation proof method
- Pretty-big-step semantics
- Program verification through characteristic formulae
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
- Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction
- Sound, modular and compositional verification of the input/output behavior of programs
- Temporary read-only permissions for separation logic
- The verified CakeML compiler backend
- Trace-Based Coinductive Operational Semantics for While
- Transfinite reductions in orthogonal term rewriting systems
- Verified characteristic formulae for CakeML
This page was built for publication: Characteristic formulae for liveness properties of non-terminating CakeML programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875446)
