formal verification, heap allocator, systems programming, isabelle, autocorres
Computer Sciences | Information Security | Software Engineering
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 code of the heap allocator is imported into Isabelle/HOL using CParser and AutoCorres. In addition to providing the guarantee that the heap allocator is free of bugs and therefore is suitable for use in security critical projects, our work facilitates verification of other projects written in C that utilize Isabelle and AutoCorres.
Sahebolamri, Arash; Constable, Scott D.; and Chapin, Steve J., "A Formally Veriﬁed Heap Allocator" (2018). Electrical Engineering and Computer Science - Technical Reports. 182.
Creative Commons License
This work is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 4.0 License.