Sciweavers

Share
ITP
2010

Separation Logic Adapted for Proofs by Rewriting

8 years 9 months ago
Separation Logic Adapted for Proofs by Rewriting
We present a formalisation of separation logic which, by avoiding the use of existential quantifiers, allows proofs that only use standard equational rewriting methods as found in off-the-shelf theorem provers. This proof automation is sufficiently strong to free the user from dealing with low-level details in proofs of functional correctness. The work presented here has been implemented in HOL4 and ACL2. It is illustrated on a standard example (reversal of a linked-list).
Magnus O. Myreen
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where ITP
Authors Magnus O. Myreen
Comments (0)
books