DocumentCode
2769950
Title
Towards Automatic Assertion Refinement for Separation Logic
Author
Ireland, Andrew
Author_Institution
Sch. of Math. & Comput. Sci., Heriot-Watt Univ., Edinburgh
fYear
2006
fDate
18-22 Sept. 2006
Firstpage
309
Lastpage
312
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
Keywords
formal logic; reasoning about programs; theorem proving; automatic assertion refinement; formal reasoning; partial correctness proofs; pointer programs; proof automation; proof patching; proof planning; separation logic; Automatic logic units; Automation; Calculus; EMP radiation effects; Hydrogen; Logic design; Programming profession; Proposals;
fLanguage
English
Publisher
ieee
Conference_Titel
Automated Software Engineering, 2006. ASE '06. 21st IEEE/ACM International Conference on
Conference_Location
Tokyo
ISSN
1938-4300
Print_ISBN
0-7695-2579-2
Type
conf
DOI
10.1109/ASE.2006.69
Filename
4019594
Link To Document