I will discuss ongoing work on verifying an incremental generational garbage collector using the PVS theorem prover. The collector is similar to one used as part of a memory management system under development at Harlequin. One hope is that Harlequin should be able to use this work as a basis for their own verification projects. Another is that the process of formalization should improve Harlequin's understanding of their system, and assist them in its future development.
This work is being done by myself and Healf Goguen at Edinburgh in collaboration with Harlequin's Memory Management group in Cambridge.