A Certified Verifier for a Fragment of Separation Logic
The work
| Title | A Certified Verifier for a Fragment of Separation Logic |
|---|---|
| Authors | Nicolas Marti; Reynald Affeldt |
| 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. 1
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Standing | endorsed |
| Approved | 2026-08-07 |
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},
url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.206.1196},
}
This record lives at https://refs.drheap.org/marti2009certified/ and will keep doing so.