Automated Verification of Practical Garbage Collectors
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 handwritten or the collectors were too simplistic to use on practical applications. The work discussed in this paper presents 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. The paper used the Boogie verification generator and the Z3 automated theorem prover to verify this assembly language code mechanically.