Towards automatic assertion refinement for separation logic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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. © 2006 IEEE.

Original languageEnglish
Title of host publicationProceedings - 21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006
Pages309-312
Number of pages4
DOIs
Publication statusPublished - 2006
Event21st IEEE/ACM International Conference on Automated Software Engineering 2006 - Tokyo, Japan
Duration: 18 Sep 200622 Sep 2006

Conference

Conference21st IEEE/ACM International Conference on Automated Software Engineering 2006
Abbreviated titleASE 2006
CountryJapan
CityTokyo
Period18/09/0622/09/06

Fingerprint Dive into the research topics of 'Towards automatic assertion refinement for separation logic'. Together they form a unique fingerprint.

  • Cite this

    Ireland, A. (2006). Towards automatic assertion refinement for separation logic. In Proceedings - 21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006 (pp. 309-312) https://doi.org/10.1109/ASE.2006.69