A Certified Verifier for a Fragment of Separation Logic
The work
| Authors | Nicolas Marti; Reynald Affeldt |
|---|---|
| Editors | |
| Type | article |
| Year | 2009 |
| Citekey | marti2009certified |
Where it appeared
| Published in | Information and Media Technologies |
|---|---|
| Volume | 4 |
| Issue | 2 |
| Pages | 304--316 |
Identifiers
| DOI | 10.11185/imt.4.304 |
|---|---|
| OpenAlex | W909064011 |
Access
| Landing page | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.206.1196 |
|---|
Abstract
Separation logic is an extension of Hoare logic to verify imperative programs with pointers and mutable datastructures. Although there exist several implementations of verifiers for separation logic, none of them has actually been itself verified. In this paper, we present a verifier for a fragment of separation logic that is verified inside the Coq proof assistant. This verifier is implemented as a Coq tactic by reflection to verify separation logic triples. Thanks to the extraction facility to OCaml, we can also derive a certified, stand-alone and efficient verifier for separation logic.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-08-16 17:12 UTC |
Filed under
Cite it as
@article{marti2009certified,
title = {A Certified Verifier for a Fragment of Separation Logic},
author = {Nicolas Marti and Reynald Affeldt},
year = {2009},
journal = {Information and Media Technologies},
volume = {4},
number = {2},
pages = {304--316},
doi = {10.11185/imt.4.304},
}
This record lives at https://refs.drheap.org/marti2009certified/ and will keep doing so.