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

DOI10.1007/s00165-009-0125-8zbMath1214.68118OpenAlexW2025897881MaRDI QIDQ607403

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

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

interferencedata refinementseparation logicpointer aliasing

Mathematics Subject Classification ID

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

Related Items (3)

Abstract local reasoning for concurrent libraries: mind the gap ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ Refactoring and representation independence for class hierarchies

Cites Work

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

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