• 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. TUCS Technical Reports 753, Turku Centre for Computer Science, 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.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tPreoteasa06a,
  title = {Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic},
  author = {Preoteasa, Viorel},
  number = {753},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2006},
  keywords = {Pointer Programs. Separation Logic. Recursive Procedures. Predicate Transformers Semantics. Mechanical Verification of Programs.},
  ISBN = {952-12-1697-2},
}

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

Edit publication