Towards mechanized program verification with separation logic
The work
| Authors | Tjark Weber |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2004 |
| Citekey | weber2004towards |
Where it appeared
| Published in | 18th International Workshop on Computer Science Logic (CSL) |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 3210 |
| Volume | 3210 |
| Pages | 250--264 |
Identifiers
| DOI | 10.1007/978-3-540-30124-0_21 |
|---|---|
| ISBN | 978-3-540-23024-3 |
Abstract
Using separation logic, this paper presents three Hoare logics (corresponding to different notions of correctness) for the simple While language extended with commands for heap access and modification. Properties of separating conjunction and separating implication are mechanically verified and used to prove soundness and relative completeness of all three Hoare logics. The whole development, including a formal proof of the Frame Rule, is carried out in the theorem prover Isabelle/HOL.
A copy is held
pdf, 140.2 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-17 08:36 UTC |
Filed under
Cite it as
@inproceedings{weber2004towards,
title = {Towards mechanized program verification with separation logic},
author = {Tjark Weber},
year = {2004},
booktitle = {18th International Workshop on Computer Science Logic (CSL)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3210},
pages = {250--264},
isbn = {978-3-540-23024-3},
doi = {10.1007/978-3-540-30124-0_21},
}
This record lives at https://refs.drheap.org/weber2004towards/ and will keep doing so.