scientific article; zbMATH DE number 2087445

zbMath1077.68705MaRDI QIDQ4738240

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: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Extending separation logic with fixpoints and postponed substitution, A stone-type duality theorem for separation logic via its underlying bunched logics, Certifying low-level programs with hardware interrupts and preemptive threads, Formal verification of C systems code. Structured types, separation logic and theorem proving, Relational separation logic, A Program Construction and Verification Tool for Separation Logic, Exploring modal worlds, Function extraction, Safe Modification of Pointer Programs in Refinement Calculus, Unnamed Item, Adjunct elimination in context logic for trees, Precision and the Conjunction Rule in Concurrent Separation Logic, Concurrent Separation Logic and Operational Semantics, Algebraic separation logic, Frame rule for mutually recursive procedures manipulating pointers, Unifying separation logic and region logic to allow interoperability, Unnamed Item, On Locality and the Exchange Law for Concurrent Processes, An adaptation-complete proof system for local reasoning about cloud storage systems, Reasoning about block-based cloud storage systems via separation logic, Separation Logic Tutorial, Modal algebra and Petri nets, On the relation between concurrent separation logic and concurrent Kleene algebra