Title :
Towards Automatic Assertion Refinement for Separation Logic
Author_Institution :
Sch. of Math. & Comput. Sci., Heriot-Watt Univ., Edinburgh
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;
Conference_Titel :
Automated Software Engineering, 2006. ASE '06. 21st IEEE/ACM International Conference on
Conference_Location :
Tokyo
Print_ISBN :
0-7695-2579-2
DOI :
10.1109/ASE.2006.69
