Local reasoning about a copying garbage collector

DOI10.1145/964001.964020zbMATH Open1325.68041OpenAlexW1975076763MaRDI QIDQ3452262FDOQ3452262

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

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

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)

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
• Title not available (Why is that?)
• A semantics for concurrent separation logic
• Higher-order separation logic in Isabelle/HOLCF
• Program logic and equivalence in the presence of garbage collection.
• Relational separation logic
• 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)