A mechanically verified incremental garbage collector

DOI10.1007/BF01211305zbMath0941.68624OpenAlexW2092767796MaRDI QIDQ1336946

David M. Russinoff

Publication date: 26 February 1996

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01211305

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos, Unnamed Item, A verified generational garbage collector for CakeML, A verified generational garbage collector for CakeML, Fine-grained concurrency with separation logic, Simplification of boolean verification conditions, Specification and verification of concurrent programs through refinements

Uses Software

• LISP
• NQTHM

Cites Work

• Adequate proof principles for invariance and liveness properties of concurrent programs
• An incremental garbage collection algorithm for multi-mutator systems
• A verification system for concurrent programs based on the Boyer-Moore prover
• Algorithms for on-the-fly garbage collection
• On-the-fly garbage collection
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item