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

You find some more material and proofs here (some material are not finished to be typed or are not well organized yet, if you wish something else please ask)

• The function ast (.ps.gz, .pdf)
• The translation function (.ps.gz, .pdf)
• Counstrains on the domain (.ps.gz, .pdf)
• why [[ . ]]' ? (.ps.gz, .pdf)
• cheap-extension (.ps.gz, .pdf)
• extension (.ps.gz, .pdf)
• CL_eq (.ps.gz, .pdf)
• CL_eq proofs(.ps.gz, .pdf)
• merging (.ps.gz, .pdf)
• replace (.ps.gz, .pdf)
• union (.ps.gz, .pdf)
• precise union example (.ps.gz, .pdf)
• widening-proof (.ps.gz, .pdf)

---

Contact: Elodie-JaneSimspolytechniqueedu Last modified: April 2010

Back