scientific article; zbMATH DE number 2087445
From MaRDI portal
Publication:4738240
zbMATH Open1077.68705MaRDI QIDQ4738240FDOQ4738240
Authors: Hongseok Yang, Peter W. O'Hearn 
Publication date: 11 August 2004
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2303/23030402.htm
Title of this publication is not available (Why is that?)
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)
Cited In (34)
- Adjunct elimination in context logic for trees
- Precision and the conjunction rule in concurrent separation logic
- Exploring modal worlds
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Stone-type dualities for separation logics
- Frame rule for mutually recursive procedures manipulating pointers
- Formal verification of C systems code. Structured types, separation logic and theorem proving
- Title not available (Why is that?)
- Abstract hidden Markov models: a monadic account of quantitative information flow
- Concurrent separation logic and operational semantics
- Function extraction
- On Local Reasoning in Verification
- Footprints in Local Reasoning
- Algebraic separation logic
- Extending separation logic with fixpoints and postponed substitution
- A stone-type duality theorem for separation logic via its underlying bunched logics
- Footprints in Local Reasoning
- Certifying low-level programs with hardware interrupts and preemptive threads
- Inference rules using local contexts
- Title not available (Why is that?)
- Unifying separation logic and region logic to allow interoperability
- On locality and the exchange law for concurrent processes
- Local reasoning for global invariants. II: Dynamic boundaries
- Relational separation logic
- A program construction and verification tool for separation logic
- Safe Modification of Pointer Programs in Refinement Calculus
- A semantic model of confinement and locality theorem
- Separation Logic Tutorial
- Semantics for local computational effects
- Modal algebra and Petri nets
- An adaptation-complete proof system for local reasoning about cloud storage systems
- Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
- Local reasoning about data update
- Reasoning about block-based cloud storage systems via separation logic
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4738240)
