An abstract domain for separation logic formulae, Élodie-Jane Sims
EAAI'06

Article ( ps.gz, pdf). © copyright notice

The proofs (appendix).

• Abstract : We present a separation logic abstract domain for static analysis by abstract interpretation. We consider separation logic with fixpoint formulae. The domain embeds shape and alias information. The main originality compared to usual shape-graphs is that we treat all values (numerical, heap locations, nil,...) the same way, thus we can have numerical summary nodes. To keep the domain as general as possible, it is parameterized by a numerical abstract domain which can be instantiated as needed. We provide a semantics in terms of sets of memory (the usual model for separation logic) and sound functions on the domain, including a widening and a union which precision/cost can be tuned to the specific needs of the context where the domain is used.
• BibTeX references:

  
  
  @inproceedings{Sims06,
      author 	=	"Sims, \'Elodie-Jane",
      title 	=	"An abstract domain for separation logic formulae",
      booktitle 	=	"Proceedings of the 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI06)",
      pages 	=	"133-148",
      year 	=	"2006",
      publisher 	=	"ENTCS",
      address 	=	"Vienna, Austria",
  } 
  

---

Contact: Elodie-JaneSimspolytechniqueedu Last modified: April 2010

Back