Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Theorem Prover Support for Pre...

Theorem Prover Support for Precondition and Correctness Calculation

Orieta Celiku, Joakim von Wright, Theorem Prover Support for Precondition and Correctness Calculation. In: 4th International Conference on Formal Engineering Methods, Lecture Notes in Computer Science 2495, 299–310, Springer-Verlag, 2002.

Abstract:

Tools for automatically extracting the conditions for which a program
is correct with respect to a precondition and postcondition can make
proving program correctness easier. We build a HOL-based tool that uses weakest preconditions and semantically derived rules to prove correctness theorems with the verification conditions as assumptions. The rules include two new rules for calculating loop preconditions and recursion correctness while taking specification variables into consideration. The programming language has (recursive) procedures, and both demonic and angelic nondeterminism, which can be used to model interaction. Program variables can be of arbitrary types. Programs with procedures are handled modularly, and proved facts about individual procedures are stored in a database available to all programs.

BibTeX entry:

@INPROCEEDINGS{pCevo02a,
  title = {Theorem Prover Support for Precondition and Correctness Calculation},
  booktitle = {4th International Conference on Formal Engineering Methods},
  author = {Celiku, Orieta and Wright, Joakim von},
  volume = {2495},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  pages = {299–310},
  year = {2002},
}

Belongs to TUCS Research Unit(s): Learning and Reasoning Lab

Publication Forum rating of this publication: level 1

Edit publication