Extending Separation Logic with Fixpoints and Postponed Substitution, Élodie-Jane Sims, AMAST'04

Article . © copyright notice, Springer-Verlag copyright notice

• 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 , 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.
• BibTeX references:

  @inproceedings{Sims04,
    author    = {{\'E}lodie-Jane Sims},
    title     = {Extending Separation Logic with Fixpoints and Postponed
                 Substitution.},
    booktitle = {AMAST},
    year      = {2004},
    pages     = {475-490},
    ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3116{\&}spage=475},
    crossref  = {amast04},
  }
  

  @proceedings{amast04,
    editor    = {Charles Rattray and
                 Savi Maharaj and
                 Carron Shankland},
    title     = {Algebraic Methodology and Software Technology, 10th International
                 Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16,
                 2004, Proceedings},
    booktitle = {AMAST},
    publisher = {Springer},
    series    = {Lecture Notes in Computer Science},
    volume    = {3116},
    year      = {2004},
    isbn      = {3-540-22381-9},
  }
  

---

Contact: Elodie-JaneSimspolytechniqueedu Last modified: April 2010

Back