Local reasoning about a copying garbage collector

DOI10.1145/964001.964020zbMath1325.68041OpenAlexW1975076763MaRDI QIDQ3452262

John C. Reynolds, Noah Torp-Smith, 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) Logic in computer science (03B70) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20)

Related Items

Practical Tactics for Separation Logic, A semantics for concurrent separation logic, Relational separation logic, Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example, Hoare type theory, polymorphism and separation, Higher-Order Separation Logic in Isabelle/HOLCF, An adaptation-complete proof system for local reasoning about cloud storage systems, Verifying a concurrent garbage collector with a rely-guarantee methodology, Reasoning about block-based cloud storage systems via separation logic