Formal proof of an integrated hardware garbage collector

Lead Research Organisation: University of Bristol
Department Name: Computer Science


The Integrated Hardware Garbage Collector is an innovative new design for hardware garbage collection which promises to significantly improve system security and reliability by replacing traditional MMUs. It achieves this by replacing the traditional flat address space memory model with a new object-based sparsely-connected memory model. This entirely prevents buffer overflow issues and similar classes of errors and vulnerabilities. In addition, it can offer real-time performance for high level languages such as Java, C# and Haskell. However, without strong guarantees of correctness the design cannot be trusted in general purpose applications. To provide these guarantees, this thesis formally proves the correctness of the IHGC design for both an abstract model and a Verilog implementation.


10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509619/1 01/10/2016 30/09/2021
1942419 Studentship EP/N509619/1 18/09/2017 31/03/2021 Edward Nutting