Kestrel Institute


Visible to the public Synthesis of Concurrent Garbage Collectors


Garbage collection is an attractive target for exploring the issues in synthesizing concurrent algorithms. The basic algorithms are tricky to get correct, and become even trickier when implemented on modern multi-core architectures. We are using Kestrel's Specware system to synthesize garbage collectors, starting from a formal specification of collection requirements. Novel features include a mixed algebraic/coalgebraic style of specification, and coalgebraically-oriented transformations that generate correct-by-construction refinements.


Visible to the public High Assurance Java Virtual Machine