Automated Verification of Practical Garbage Collectors
Chris Hawblitzel (Microsoft), Erez Petrank (Technion)

TL;DR
This paper presents two practically verified garbage collectors for real-world C# applications, using formal methods and automated theorem proving to ensure correctness and performance.
Contribution
It introduces two mechanically verified garbage collectors implemented in assembly, verified with Boogie and Z3, suitable for real-world use and benchmarked against standard collectors.
Findings
Verified collectors are competitive in performance.
Use of formal verification ensures correctness.
Applicable to real-world C# benchmarks.
Abstract
Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the proofs were hand-written or the collectors were too simplistic to use on practical applications. In this work, we present two mechanically verified garbage collectors, both practical enough to use for real-world C# benchmarks. The collectors and their associated allocators consist of x86 assembly language instructions and macro instructions, annotated with preconditions, postconditions, invariants, and assertions. We used the Boogie verification generator and the Z3 automated theorem prover to verify this assembly language code mechanically. We provide measurements comparing the performance of the verified collector with that of the standard…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
