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

• Type: Conference
• Year: 2004
• Where: CSL
• Authors: Tjark Weber
• Keywords: Automated Reasoning, CSL 2004, Hoare Logics, Separation Logic, Simple While Language