Blaming the client: on data refinement in the presence of pointers

DOI10.1007/S00165-009-0125-8zbMATH Open1214.68118OpenAlexW2025897881MaRDI QIDQ607403FDOQ607403

Peter W. O'Hearn, Noah Torp-Smith, Ivana Filipović, Hongseok Yang

Publication date: 22 November 2010

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-009-0125-8

zbMATH Keywords

interferenceseparation logicdata refinementpointer aliasing

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Theory of software (68N99)

Cites Work

• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• A semantics for concurrent separation logic
• Proof of correctness of data representations
• Resources, concurrency, and local reasoning
• Title not available (Why is that?)
• Programming Languages and Systems
• Title not available (Why is that?)
• Ownership confinement ensures representation independence for object-oriented programs
• Abstracting Allocation
• Separation logic and abstraction
• Specification and verification challenges for sequential object-oriented programs
• Typed Lambda Calculi and Applications
• Title not available (Why is that?)
• Relational separation logic
• Title not available (Why is that?)
• Data refinement of predicate transformers
• Calculational derivation of pointer algorithms from tree operations
• On assertion-based encapsulation for object invariants and simulations
• Generic commands--a tool for partial correctness formalisms
• Title not available (Why is that?)
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Programming Languages and Systems
• Relational Parametricity and Separation Logic

Cited In (4)

• Abstract local reasoning for concurrent libraries: mind the gap
• Refactoring and representation independence for class hierarchies
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Stepwise refinement of heap-manipulating code in Chalice

   Recommendations

• Programming Languages and Systems 👍 👎
• Title not available (Why is that?) 👍 👎
• Data Refinement with Probability in Mind 👍 👎
• A single complete rule for data refinement 👍 👎
• Data Refinement 👍 👎

This page was built for publication: Blaming the client: on data refinement in the presence of pointers

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