Steve J. Chapin

A Formally Verified Heap Allocator

2018 · Syracuse University Libraries (Syracuse University)

We present the formal verification of a heap allocator written in C. We use the Isabelle/HOL proof assistant to formally verify the correctness of the heap allocator at the source code level. The C source …