Dynamic separation logic

DOI10.46298/ENTICS.12297MaRDI QIDQ6831474zbMATH OpenFDO

Authors Frank S. de Boer, Hans-Dieter A. Hiep, Stijn De Gouw

Publication date 2 April 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/ENTICS.12297

zbMATH Keywords

dynamic logicseparation logicsequential programsweakest precondition

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites work

• A complete axiomatisation for quantifier-free separation logic
• A decision procedure for separation logic in SMT
• A first-order logic with frames
• Backwards and forwards with separation logic
• Classical mathematics for a constructive world
• Completeness and expressiveness of pointer program verification by separation logic
• Completeness for recursive procedures in separation logic
• First-order dynamic logic
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Permission-based separation logic for multithreaded Java programs

This page was built for publication: Dynamic separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6831474)