scientific article; zbMATH DE number 2087445

MaRDI QIDQ4738240zbMATH OpenFDO

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

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1841809
• Semantical analysis of specification logic. II
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Footprints in Local Reasoning
• Footprints in Local Reasoning

Cited in

(34)

• Adjunct elimination in context logic for trees
• Exploring modal worlds
• Precision and the conjunction rule in concurrent separation logic
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Frame rule for mutually recursive procedures manipulating pointers
• Stone-type dualities for separation logics
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• Function extraction
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Abstract hidden Markov models: a monadic account of quantitative information flow
• Concurrent separation logic and operational semantics
• Footprints in Local Reasoning
• On Local Reasoning in Verification
• 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
• scientific article; zbMATH DE number 5589211 (Why is no real title available?)
• Relational separation logic
• Unifying separation logic and region logic to allow interoperability
• On locality and the exchange law for concurrent processes
• A program construction and verification tool for separation logic
• Local reasoning for global invariants. II: Dynamic boundaries
• 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
• Local reasoning about data update
• Reasoning about block-based cloud storage systems via separation logic
• Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis

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)