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

DOI10.1007/S00165-009-0125-8MaRDI QIDQ607403zbMATH OpenOpenAlexFDO

Authors Ivana Filipović, Noah Torp-Smith, 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

interferenceseparation logicdata refinementpointer aliasing

Mathematics Subject Classification ID

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

Recommendations

• Programming Languages and Systems
• scientific article; zbMATH DE number 3943003
• Data refinement with probability in mind
• A single complete rule for data refinement
• Data Refinement

Cites work

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

Cited in

(5)

• 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
• Programming Languages and Systems

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)