Extending Separation Logic with Fixpoints and Postponed Substitution
The work
| Title | Extending Separation Logic with Fixpoints and Postponed Substitution |
|---|---|
| Authors | Élodie-Jane Sims |
| Type | conference paper |
| Year | 2004 |
| Citekey | sims2004extending |
Where it appeared
| Published in | Algebraic Methodology and Software Technology |
|---|---|
| Publisher | Springer |
| Pages | 475--490 |
Abstract
We are interested in static analysis of programs which use shared mutable data structures. We introduce a backward and a forward analyses with a separation logic called BIμν. This logic is an extension of BI logic [7], to which we add fixpoint connectives and a postponed substitution. This allows us to express recursive definitions within the logic as well as the axiomatic semantics of while statements. Unlike the existing rule-based approach to program proof using separation logic, our approach does not have syntactical restrictions on the use of rules.
Where this came from
| How it got here | the agent went looking · found via bibtex |
|---|---|
| First seen | 2026-08-05 |
| Standing | endorsed |
| Approved | 2026-08-07 |
Cite it as
@inproceedings{sims2004extending,
title = {Extending Separation Logic with Fixpoints and Postponed Substitution},
author = {Élodie-Jane Sims},
year = {2004},
booktitle = {Algebraic Methodology and Software Technology},
pages = {475--490},
publisher = {Springer},
}
This record lives at https://refs.drheap.org/sims2004extending/ and will keep doing so.