21st IEEE International Conference on Automated Software Engineering (ASE'06) Towards Automatic Assertion Refinement for Separation Logic Tokyo, Japan September 18-September 22 ISBN: 0-7695-2579-2
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASE.2006.69
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.
Citation:
Andrew Ireland, "Towards Automatic Assertion Refinement for Separation Logic," ase, pp.309-312, 21st IEEE International Conference on Automated Software Engineering (ASE'06), 2006 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||