Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Applying PVS Background Theori...

Applying PVS Background Theories and Proof Strategies in Invariant Based Programming

Johannes Eriksson, Ralph-Johan Back, Applying PVS Background Theories and Proof Strategies in Invariant Based Programming. In: Jin Song Dong, Huibiao Zhu (Eds.), Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings., Lecture Notes in Computer Science 6447, 24–39, Springer, 2010.

http://dx.doi.org/10.1007/978-3-642-16901-4_4

Abstract:

Invariant Based Programming (IBP) is a formal method in which the invariants are developed before the code. IBP leads to programs that are correct by construction, provides a light formalism that is easy to learn, and supports teaching formal methods. However, like other verification methods it generates a large number of lemmas to be proved. The Socos tool provides automatic verification of invariant based programs: it sends the proof obligations to an automatic theorem prover and reports only the unproven conditions. The latter may be proved interactively in a proof assistant. In this paper, we describe the Socos embedding of invariant based programs into the theorem prover PVS. The tool generates verification conditions and applies a strategy to decompose the conditions into fine grained lemmas. Each lemma is then attacked with the SMT solver Yices. Socos supports incremental development and allows reasoning in arbitrary program domains through the use of background theories. A background theory is a PVS theory pertaining to a specific programming domain. We give an example of a verification in our system, which demonstrates how background theories improve the degree of proof automation. This work is a step towards scaling up IBP by allowing existing collections of PVS theories to be used.

BibTeX entry:

@INPROCEEDINGS{iErBa10a,
  title = {Applying PVS Background Theories and Proof Strategies in Invariant Based Programming},
  booktitle = {Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings.},
  author = {Eriksson, Johannes and Back, Ralph-Johan},
  volume = {6447},
  series = {Lecture Notes in Computer Science},
  editor = {Dong, Jin Song and Zhu, Huibiao},
  publisher = {Springer},
  pages = {24–39},
  year = {2010},
}

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

Publication Forum rating of this publication: level 1

Edit publication