Formal proof of an integrated hardware garbage collector

集成硬件垃圾收集器是一种创新的硬件垃圾收集设计，有望通过取代传统的MMU来显着提高系统的安全性和可靠性。它通过用一种新的基于对象的稀疏连接内存模型取代传统的平面地址空间内存模型来实现这一点。这完全防止了缓冲区溢出问题以及类似的错误和漏洞。此外，它还可以为Java、C#和Haskell等高级语言提供实时性能。然而，如果没有强有力的正确性保证，在通用应用程序中就不能信任该设计。为了提供这些保证，本文正式证明了IHGC设计的正确性的抽象模型和Verilog实现。

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.