Verifying a concurrent garbage collector using a rely-guarantee methodology

DOI10.1007/978-3-319-66107-0_31MaRDI QIDQ1687774zbMATH OpenOpenAlexFDO

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

Publication date 4 January 2018

Full work available at URL https://hal.inria.fr/hal-01613389/file/itp17.pdf

Mathematics Subject Classification ID

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

Recommendations

• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Formal Verification of an Incremental Garbage Collector
• Formal verification of a lock-free stack with hazard pointers
• scientific article; zbMATH DE number 1956564
• A verified generational garbage collector for CakeML

Cites work

• scientific article; zbMATH DE number 1956564 (Why is no real title available?)
• A Marriage of Rely/Guarantee and Separation Logic
• A calculus of atomic actions
• A certified framework for compiling and executing garbage-collected languages
• Automated verification of practical garbage collectors
• Concurrent separation logic and operational semantics
• On-the-fly garbage collection
• Tentative steps toward a development method for interfering programs
• Verifying a concurrent garbage collector using a rely-guarantee methodology

Cited in

(8)

• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
• A rely-guarantee-based simulation for verifying concurrent program transformations
• A verified generational garbage collector for CakeML
• Formal derivation of concurrent garbage collectors
• A verified generational garbage collector for CakeML
• Verifying a concurrent garbage collector using a rely-guarantee methodology
• scientific article; zbMATH DE number 1670550 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

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

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