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

An Algebraic Treatment of Procedure Refinement to Support Mechanical Verification

Ralph-Johan Back, Viorel Preoteasa, An Algebraic Treatment of Procedure Refinement to Support Mechanical Verification. Formal Aspects of Computing 17(1), 69 – 90, 2005.

http://dx.doi.org/10.1007/s00165-004-0060-7

Abstract:

We introduce a new algebraic model for program variables, suitable
for reasoning about recursive procedures with parameters and local
variables in a mechanical verification setting.
We give a predicate transformer semantics to recursive
procedures and prove refinement rules for introducing recursive procedure
calls, procedure parameters, and local variables. We also prove, based on
the refinement rules, Hoare total correctness rules for recursive procedures,
and parameters. We introduce a special form of Hoare specification statement
which alone is enough to fully specify a procedure. Moreover, we prove that this
Hoare specification statement is equivalent to a refinement specification. We
implemented this theory in the PVS theorem prover.

Files:

Full publication in PDF-format

BibTeX entry:

@ARTICLE{jBaPr05a,
  title = {An Algebraic Treatment of Procedure Refinement to Support Mechanical Verification},
  author = {Back, Ralph-Johan and Preoteasa, Viorel},
  journal = {Formal Aspects of Computing},
  volume = {17},
  number = {1},
  publisher = {Springer},
  pages = {69 – 90},
  year = {2005},
  keywords = {Refinement, Recursive procedures, Semantics, Hoare logic, Mechanical verification},
}

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

Publication Forum rating of this publication: level 2

Edit publication