Towards Mechanized Program Verification with Separation Logic

Tjark Weber. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic - 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 250-264. Springer, September 2004.

Abstract

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.

Download

• PDF (140 kB)

BibTeX

@inproceedings{weber04towards,
  author    = {Tjark Weber},
  title     = {Towards Mechanized Program Verification with Separation Logic},
  editor    = {Jerzy Marcinkowski and Andrzej Tarlecki},
  booktitle = {Computer Science Logic~-- 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 2004, Proceedings},
  volume    = {3210},
  series    = {Lecture Notes in Computer Science},
  pages     = {250--264},
  publisher = {Springer},
  month     = sep,
  year      = {2004},
  isbn      = {3-540-23024-6}
}