Verifying a concurrent garbage collector using a rely-guarantee methodology

DOI10.1007/978-3-319-66107-0_31zbMath1468.68067MaRDI 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

68N20: Theory of compilers and interpreters

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Related Items

A verified generational garbage collector for CakeML, 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

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