Local reasoning about a copying garbage collector

DOI10.1145/964001.964020MaRDI QIDQ3452262zbMATH OpenOpenAlexFDO

Authors Noah Torp-Smith, John C. Reynolds, Lars Birkedal

Publication date 11 November 2015

Published in Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/964001.964020

zbMATH Keywords

separation logiclocal reasoningcopying garbage collector

Mathematics Subject Classification ID

Theory of programming languages (68N15) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 1701349
• Program logic and equivalence in the presence of garbage collection.
• Higher-order separation logic in Isabelle/HOLCF
• Formal models of distributed memory management
• Formal Verification of an Incremental Garbage Collector

Cited in

(12)

• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
• scientific article; zbMATH DE number 1701349 (Why is no real title available?)
• A semantics for concurrent separation logic
• Higher-order separation logic in Isabelle/HOLCF
• Relational separation logic
• Program logic and equivalence in the presence of garbage collection.
• Practical Tactics for Separation Logic
• Formal models of distributed memory management
• An adaptation-complete proof system for local reasoning about cloud storage systems
• Reasoning about block-based cloud storage systems via separation logic
• Hoare type theory, polymorphism and separation

This page was built for publication: Local reasoning about a copying garbage collector

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