• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic

Viorel Preoteasa, Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic. In: FM 2006: Formal Methods, 14th International Symposium on Formal Methods Hamilton, Canada, August 21-27, 2006 Proceedings, Lecture Notes in Computer Science 4085, 508 – 523, Springer Berlin / Heidelberg, 2006.

Abstract:

Using a predicate transformer semantics of programs, we introduce
statements for heap operations and separation logic operators for specifying programs
that manipulate pointers. We prove consistent Hoare total correctness rules
for pointer manipulating statements according to the predicate
transformer semantics. We prove the frame rule in the context of a programming language with
recursive procedures with value and result parameters and local variables, where program variables and addresses can
store values of any type of the theorem prover.
The theory, including the proofs, is implemented in
the theorem prover PVS.

BibTeX entry:

@INPROCEEDINGS{inpPreoteasa06a,
  title = {Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic},
  booktitle = {FM 2006: Formal Methods, 14th International Symposium on Formal Methods Hamilton, Canada, August 21-27, 2006 Proceedings},
  author = {Preoteasa, Viorel},
  volume = {4085},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Berlin / Heidelberg},
  pages = {508 – 523},
  year = {2006},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Publication Forum rating of this publication: level 1

Edit publication