Sciweavers

Share
CSL
2004
Springer

Towards Mechanized Program Verification with Separation Logic

12 years 3 months ago
Towards Mechanized Program Verification with Separation Logic
Using separation logic, this paper presents three Hoare logics (corresponding to different notions of correctness) for the simple While language extended with commands for heap access and modification. Properties of separating conjunction and separating implication are mechanically verified and used to prove soundness and relative completeness of all three Hoare logics. The whole development, including a formal proof of the Frame Rule, is carried out in the theorem prover Isabelle/HOL. Keywords. Separation Logic, Formal Program Verification, Interactive Theorem Proving
Tjark Weber
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where CSL
Authors Tjark Weber
Comments (0)
books