Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 1 of 1
Full-Text Articles in Physical Sciences and Mathematics
A Formally Verified Heap Allocator, Arash Sahebolamri, Scott D. Constable, Steve J. Chapin
A Formally Verified Heap Allocator, Arash Sahebolamri, Scott D. Constable, Steve J. Chapin
Electrical Engineering and Computer Science - Technical Reports
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.