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

Frame Rule for Mutually Recursive Procedures Manipulating Pointers

Viorel Preoteasa, Frame Rule for Mutually Recursive Procedures Manipulating Pointers . Theoretical Computer Science 410(42), 4216–4233 , 2009.

http://dx.doi.org/10.1016/j.tcs.2009.05.016

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 a powerful Hoare total correctness rule for mutually recursive procedures manipulating pointers. The rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. The theory, including the proofs, is implemented in the theorem prover PVS. In this implementation program variables and addresses can store values of almost any type of the theorem prover.

Files:

Full publication in PDF-format

BibTeX entry:

@ARTICLE{jPreoteasa09a,
  title = {Frame Rule for Mutually Recursive Procedures Manipulating Pointers },
  author = {Preoteasa, Viorel},
  journal = {Theoretical Computer Science},
  volume = {410},
  number = {42},
  pages = {4216–4233 },
  year = {2009},
  keywords = {Predicate transformer semantics; Mechanical verification of programs; Mutually recursive procedures; Pointers; Separation logic; Frame rule},
}

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

Publication Forum rating of this publication: level 2

Edit publication