CRASH Project

The CRASH project focuses on the automated synthesis of Concurrent Garbage Collectors, starting with formal requirements-level specifications. Novel developments include: (i) techniques for specifying interacting processes using mixtures of algebraic and coalgebraic operations, (ii) novel algorithm theories (with proofs) to enable the automated synthesis of fixpoint algorithms that operate concurrently with other state-changing processes, and (iii) transformations for generating refinements of coalgebraic specifications. Working garbage collectors have been generated, and current work involves extending the transformations to emit proofs.