Characteristic formulae for liveness properties of non-terminating CakeML programs
From MaRDI portal
Publication:5875446
DOI10.4230/LIPIcs.ITP.2019.32OpenAlexW2977469202MaRDI QIDQ5875446
Magnus O. Myreen, Pohjola Johannes Åman, Henrik Rostedt
Publication date: 3 February 2023
Full work available at URL: https://doi.org/10.4230/LIPIcs.ITP.2019.32
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Flag-based big-step semantics
- Coinductive big-step operational semantics
- Non-standard semantics for program slicing
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
- Transfinite reductions in orthogonal term rewriting systems
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
- A formally verified compiler back-end
- Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs
- Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
- Temporary Read-Only Permissions for Separation Logic
- Verified Characteristic Formulae for CakeML
- Trace-Based Coinductive Operational Semantics for While
- A Dynamic Logic with Traces and Coinduction
- A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While
- On the bisimulation proof method
- The verified CakeML compiler backend
- Program verification through characteristic formulae
- Characteristic formulae for the verification of imperative programs
- Pretty-Big-Step Semantics
