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

• A calculus of atomic actions
• A certified framework for compiling and executing garbage-collected languages
• A Marriage of Rely/Guarantee and Separation Logic
• Automated verification of practical garbage collectors
• Concurrent separation logic and operational semantics
• scientific article; zbMATH DE number 1956564 (Why is no real title available?)
• 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

(9)

• Verifying a concurrent garbage collector using a rely-guarantee methodology
• 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 1670550 (Why is no real title available?)
• A rely-guarantee-based simulation for verifying concurrent program transformations
• Formal derivation of concurrent garbage collectors
• A verified generational garbage collector for CakeML
• A verified generational garbage collector for CakeML
• A mechanically verified garbage collector for OCaml

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)