Title

A Formally Verified Heap Allocator

Author(s)/Creator(s)

Arash Sahebolamri, Syracuse UniversityFollow
Scott D. Constable, Syracuse UniversityFollow
Steve J. Chapin, Syracuse UniversityFollow

Document Type

Report

Date

2018

Keywords

formal verification, heap allocator, systems programming, isabelle, autocorres

Language

English

Disciplines

Computer Sciences | Information Security | Software Engineering

Description/Abstract

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.

Additional Information

Licensing information:

Creative Commons CC-BY-NC-ND

Recommended Citation

Sahebolamri, Arash; Constable, Scott D.; and Chapin, Steve J., "A Formally Verified Heap Allocator" (2018). Electrical Engineering and Computer Science - Technical Reports. 182.
https://surface.syr.edu/eecs_techreports/182

Source

submission

Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.