Towards automatic assertion refinement for separation logic

Andrew Ireland

doi:10.1109/ASE.2006.69

Towards automatic assertion refinement for separation logic

Andrew Ireland

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

11 Citations (Scopus)

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 language	English
Title of host publication	Proceedings - 21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006
Pages	309-312
Number of pages	4
DOIs	https://doi.org/10.1109/ASE.2006.69
Publication status	Published - 2006
Event	21st IEEE/ACM International Conference on Automated Software Engineering 2006 - Tokyo, Japan Duration: 18 Sept 2006 → 22 Sept 2006

Conference

Conference	21st IEEE/ACM International Conference on Automated Software Engineering 2006
Abbreviated title	ASE 2006
Country/Territory	Japan
City	Tokyo
Period	18/09/06 → 22/09/06

Access to Document

10.1109/ASE.2006.69

Cite this

@inproceedings{6d845832c11747aabb6c74cdddaf7156,

title = "Towards automatic assertion refinement for separation logic",

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. {\textcopyright} 2006 IEEE.",

author = "Andrew Ireland",

year = "2006",

doi = "10.1109/ASE.2006.69",

language = "English",

isbn = "0769525792",

pages = "309--312",

booktitle = "Proceedings - 21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006",

note = "21st IEEE/ACM International Conference on Automated Software Engineering 2006, ASE 2006 ; Conference date: 18-09-2006 Through 22-09-2006",

}

TY - GEN

T1 - Towards automatic assertion refinement for separation logic

AU - Ireland, Andrew

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=34547435107&partnerID=8YFLogxK

U2 - 10.1109/ASE.2006.69

DO - 10.1109/ASE.2006.69

M3 - Conference contribution

SN - 0769525792

SN - 9780769525792

SP - 309

EP - 312

BT - Proceedings - 21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006

T2 - 21st IEEE/ACM International Conference on Automated Software Engineering 2006

Y2 - 18 September 2006 through 22 September 2006

ER -

Towards automatic assertion refinement for separation logic

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this