Extending Separation Logic with Fixpoints and Postponed Substitution, Élodie-Jane Sims
journal of Theoretical Computer Science Vol. 351, Issue 2

Article (modified from the publisher version: ps.gz, pdf). © copyright notice, Elsevir

The proofs (appendix).

• Abstract : We are interested in separation-logic-based static analysis of programs that use shared mutable data structures. In this paper, we introduce backward and forward analysis for a separation logic called BIμν, an extension of separation logic [Ishtiaq \& O'Hearn, POPL'01], to which we add fixpoint connectives and postponed substitution. This allows us to express recursive definitions within the logic as well as the axiomatic semantics of while statements.
• BibTeX references:

  
  @article{Sims05,
  author = {Sims, \'Elodie-Jane},
     title  = {Extending Separation Logic with Fixpoints and Postponed
     Substitution},
  year = "2006",
  journal="Theoretical Computer Science",
  volume="351",
  number    = {2},
  year      = {2006},
  pages     = {258-275}
  }
  

---

Contact: Elodie-JaneSimspolytechniqueedu Last modified: April 2010

Back