Abstract
We present a programming language, model, and logic appropriate for implementing and reasoning
about a memory management system. We state semantically what is meant by correctness of a
copying garbage collector, and employ a variant of the novel separation logics to formally specify
partial correctness of Cheney’s copying garbage collector in our program logic. Finally, we prove
that our implementation of Cheney’s algorithm meets its specification using the logic we have given
and auxiliary variables.
Udgivelsesdato: 2008
about a memory management system. We state semantically what is meant by correctness of a
copying garbage collector, and employ a variant of the novel separation logics to formally specify
partial correctness of Cheney’s copying garbage collector in our program logic. Finally, we prove
that our implementation of Cheney’s algorithm meets its specification using the logic we have given
and auxiliary variables.
Udgivelsesdato: 2008
| Originalsprog | Engelsk |
|---|---|
| Tidsskrift | ACM Transactions on Programming Languages and Systems |
| Vol/bind | 30 |
| Udgave nummer | 4 |
| Sider (fra-til) | 24-81 |
| Antal sider | 58 |
| ISSN | 0164-0925 |
| Status | Udgivet - 2008 |
Emneord
- Realiability
- Theory
- Verification
- Separation Logic
- Copying Garbage Collector
- Local Reasoning