Sound Automation of Magic Wands

DOI10.1007/978-3-031-13188-2_7MaRDI QIDQ6487333zbMATH OpenFDO

Authors Thibault Dardinier, Peter Müller, Alexander J. Summers

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-13188-2_7

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• On the almighty wand
• Strong-separation logic
• On the Almighty Wand
• A proof system for separation logic with magic wand
• Frame inference for inductive entailment proofs in separation logic

Cites work

• A proof system for separation logic with magic wand
• Caper
• Expressive modular fine-grained concurrency specification
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Logical reasoning for disjoint permissions
• Modular reasoning for deterministic parallelism
• On the almighty wand
• Reasoning over permissions regions in concurrent separation logic
• Relational inductive shape analysis
• Separation logic and abstraction
• Sound Automation of Magic Wands
• The relationship between separation logic and implicit dynamic frames
• Viper: a verification infrastructure for permission-based reasoning

Cited in

(4)

• Sound Automation of Magic Wands
• Unbounded Separation Logic
• A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand
• Formalization of a Framework for the Sound Automation of Magic Wands

This page was built for publication: Sound Automation of Magic Wands

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