Multimodal Separation Logic for Reasoning About Operational Semantics
From MaRDI portal
Publication:5415628
DOI10.1016/j.entcs.2008.10.002zbMath1286.68395OpenAlexW2134194297MaRDI QIDQ5415628
Robert Dockins, Andrew W. Appel, Aquinas Hobor
Publication date: 13 May 2014
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2008.10.002
Theory of programming languages (68N15) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (2)
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Resources, concurrency, and local reasoning
- Application of modal logic to programming
- A guide to completeness and complexity for modal logics of knowledge and belief
- A syntactic approach to type soundness
- Mathematical modal logic: A view of its evolution
- A list-machine benchmark for mechanized metatheory
- A very modal model of a modern, major, general type system
- Context logic as modal logic
- Local Reasoning for Storable Locks and Threads
- Separation Logic for Small-Step cminor
- Dynamic Logic with Non-rigid Functions
- An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
- Formal Verification of an Incremental Garbage Collector
- BI as an assertion language for mutable data structures
- Oracle Semantics for Concurrent Separation Logic
- Theorem Proving in Higher Order Logics
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Multimodal Separation Logic for Reasoning About Operational Semantics
