Towards Automatic Assertion Refinement for Separation Logic

DOI 10.1109/ase.2006.69 dblp

Abstract

Separation logic holds the promise of supporting scalable formal reasoning for pointer programs. Here we consider proof automation for separation logic. In particular we propose an approach to automating partial correctness proofs for recursive procedures. Our proposal is based upon proof planning and proof patching via assertion refinement

BibTeX

@inproceedings{Ireland:ASE06,
  author    = {Andrew Ireland},
  title     = {Towards Automatic Assertion Refinement for Separation Logic},
  booktitle = {ASE},
  pages     = {309--312},
  publisher = {{IEEE} Computer Society},
  year      = {2006},
}

Towards Automatic Assertion Refinement for Separation Logic

Abstract

Related papers