@inproceedings{df2874688f4d4f1b88783d1a3c93f733,
title = "Verified sequential Malloc/Free",
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.",
keywords = "formal verification, memory management, separation logic",
author = "Appel, {Andrew W.} and Naumann, {David A.}",
note = "Publisher Copyright: {\textcopyright} 2020 ACM.; 19th ACM SIGPLAN International Symposium on Memory Management, ISMM 2020, in conjunction with PLDI 2020 ; Conference date: 16-06-2020",
year = "2020",
month = jun,
day = "16",
doi = "10.1145/3381898.3397211",
language = "English",
series = "International Symposium on Memory Management, ISMM",
pages = "48--59",
editor = "Chen Ding and Martin Maas",
booktitle = "ISMM 2020 - Proceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management, co-located with PLDI 2020",
}