Verified sequential Malloc/Free

Andrew W. Appel, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

10 Scopus citations

Abstract

We verify the functional correctness of an array-of-bins (segregated free-lists) single-thread malloc/free system with respect to a correctness specification written in separation logic. The memory allocator is written in standard C code compatible with the standard API; the specification is in the Verifiable C program logic, and the proof is done in the Verified Software Toolchain within the Coq proof assistant. Our "resource-aware" specification can guarantee when malloc will successfully return a block, unlike the standard Posix specification that allows malloc to return NULL whenever it wants to. We also prove subsumption (refinement): the resource-aware specification implies a resource-oblivious spec.

Original languageEnglish
Title of host publicationISMM 2020 - Proceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management, co-located with PLDI 2020
EditorsChen Ding, Martin Maas
Pages48-59
Number of pages12
ISBN (Electronic)9781450375665
DOIs
StatePublished - 16 Jun 2020
Event19th ACM SIGPLAN International Symposium on Memory Management, ISMM 2020, in conjunction with PLDI 2020 - London, United Kingdom
Duration: 16 Jun 2020 → …

Publication series

NameInternational Symposium on Memory Management, ISMM

Conference

Conference19th ACM SIGPLAN International Symposium on Memory Management, ISMM 2020, in conjunction with PLDI 2020
Country/TerritoryUnited Kingdom
CityLondon
Period16/06/20 → …

Keywords

  • formal verification
  • memory management
  • separation logic

Fingerprint

Dive into the research topics of 'Verified sequential Malloc/Free'. Together they form a unique fingerprint.

Cite this