Verifying a concurrent garbage collector with a rely-guarantee methodology

DOI10.1007/s10817-018-9489-xzbMath1468.68068OpenAlexW2899108093MaRDI QIDQ2319995

Delphine Demange, David Cachera, Yannick Zakowski, Suresh Jagannathan, Gustavo Petri, Jan Vitek, David Pichardie

Publication date: 21 August 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-9489-x

zbMATH Keywords

concurrencyCoqrely-guaranteeverified garbage collection

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• z3
• Boogie
• CompCertTSO
• Milawa
• Jitawa
• GCminor

Cites Work

• Unnamed Item
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• A semantics for concurrent separation logic
• An axiomatic proof technique for parallel programs
• Verifying a concurrent garbage collector using a rely-guarantee methodology
• Plan B
• A rely-guarantee-based simulation for verifying concurrent program transformations
• Local reasoning about a copying garbage collector
• A Marriage of Rely/Guarantee and Separation Logic
• Formal Derivation of Concurrent Garbage Collectors
• Tentative steps toward a development method for interfering programs
• On-the-fly garbage collection
• A certified framework for compiling and executing garbage-collected languages
• A calculus of atomic actions
• Automated verification of practical garbage collectors
• CompCertTSO
• Concurrent Separation Logic and Operational Semantics
• A verified generational garbage collector for CakeML

This page was built for publication: Verifying a concurrent garbage collector with a rely-guarantee methodology