A semantic basis for local reasoning

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

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

Recommendations

• Local reasoning about programs that alter data structures
• 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

(40)

• Unifying separation logic and region logic to allow interoperability
• An adaptation-complete proof system for local reasoning about cloud storage systems
• Reasoning about block-based cloud storage systems via separation logic
• A stone-type duality theorem for separation logic via its underlying bunched logics
• Modal algebra and Petri nets
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Semantics for local computational effects
• Local reasoning about data update
• A program construction and verification tool for separation logic
• On locality and the exchange law for concurrent processes
• Stone-type dualities for separation logics
• A semantic model of confinement and locality theorem
• Safe Modification of Pointer Programs in Refinement Calculus
• Footprints in Local Reasoning
• Exploring modal worlds
• Function extraction
• Local reasoning about programs that alter data structures
• scientific article; zbMATH DE number 5589211 (Why is no real title available?)
• Abstract hidden Markov models: a monadic account of quantitative information flow
• Local reasoning for global invariants. II: Dynamic boundaries
• On Local Reasoning in Verification
• Footprints in Local Reasoning
• Algebraic separation logic
• Separation Logic Tutorial
• Precision and the conjunction rule in concurrent separation logic
• Concurrent separation logic and operational semantics
• Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
• A generalised union of rely-guarantee and separation logic using permission algebras
• Equivalence and conditional independence in atomic sheaf logic
• Safety, relative tightness and the probabilistic frame rule
• Frame rule for mutually recursive procedures manipulating pointers
• Probabilistic predicate transformers. II: Partially observable probability
• Formalization of Refinement Calculus for Reactive Systems
• Algebra of Monotonic Boolean Transformers
• Inference rules using local contexts
• Extending separation logic with fixpoints and postponed substitution
• 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
• Adjunct elimination in context logic for trees

This page was built for publication: A semantic basis for local reasoning

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