Verifying a concurrent garbage collector using a rely-guarantee methodology

DOI10.1007/978-3-319-66107-0_31zbMath1468.68067OpenAlexW2747080245MaRDI QIDQ1687774

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

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) 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)

Related Items (4)

Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example ⋮ Verifying a concurrent garbage collector using a rely-guarantee methodology ⋮ A verified generational garbage collector for CakeML ⋮ Verifying a concurrent garbage collector with a rely-guarantee methodology

Uses Software

• Coq

Cites Work

• Unnamed Item
• Verifying a concurrent garbage collector using a rely-guarantee methodology
• A Marriage of Rely/Guarantee and Separation Logic
• 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
• Concurrent Separation Logic and Operational Semantics

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