Tech Reports Home Contact
Technical Report Series
Actions
Submit Report
Browse Reports
Information
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0039


TitleTowards Automatic Assertion Refinement for Separation Logic
AuthorsAndrew Ireland
Date2006-06-16
AbstractSeparation 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.
GroupDependable Systems
Notes
Download

 

Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 Copyright Heriot-Watt University, Disclaimer