Formal Verification of an Incremental Garbage Collector

DOI10.1093/LOGCOM/13.6.815MaRDI QIDQ4812315zbMATH OpenOpenAlexFDO

Authors Solange Coupet-Grimal, Catherine Nouvet

Publication date 7 September 2004

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/13.6.815

zbMATH Keywords

formal methodstype theorytemporal logicsco-inductiongarbage collectors

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Temporal logic (03B44)

Recommendations

• scientific article; zbMATH DE number 1759448
• scientific article; zbMATH DE number 1696614
• Verifying a concurrent garbage collector with a rely-guarantee methodology
• A verified generational garbage collector for CakeML
• A verified generational garbage collector for CakeML

Cited in

(13)

• Local reasoning about a copying garbage collector
• Verifying a concurrent garbage collector with a rely-guarantee methodology
• scientific article; zbMATH DE number 1696614 (Why is no real title available?)
• Automated verification of practical garbage collectors
• Multimodal Separation Logic for Reasoning About Operational Semantics
• A Coq library for verification of concurrent programs
• scientific article; zbMATH DE number 1759448 (Why is no real title available?)
• Automated verification of practical garbage collectors
• Formal derivation of concurrent garbage collectors
• Verifying a concurrent garbage collector using a rely-guarantee methodology
• Improving flow analyses via ΓCFA
• scientific article; zbMATH DE number 1670550 (Why is no real title available?)
• A verified specification of TLSF memory management allocator using state monads

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Formal Verification of an Incremental Garbage Collector

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