Characteristic formulae for liveness properties of non-terminating CakeML programs

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

zbMATH Keywords

livenessHoare logicprogram verificationnon-termination

Mathematics Subject Classification ID

Uses Software

• JML
• seL4

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

This page was built for publication: Characteristic formulae for liveness properties of non-terminating CakeML programs