Verification of a Generational Garbage Collector

Shengyi Wang, Kathrin Stark, Andrew W. Appel

We have formally verified in Rocq+VST a multi-generation collector with support for mutable references, written in C and compatible with OCaml data types. Its carefully specified A…