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

Verification and Code Generation for Invariant Diagrams in Isabelle

Viorel Preoteasa, Ralph-Johan Back, Johannes Eriksson, Verification and Code Generation for Invariant Diagrams in Isabelle. In: Paul Petterson, Cristina Seceleanu (Eds.), Proceedings of the 23rd Nordic Workshop on Programming Theory, 30--32, Mälardalen Real-Time Research Centre, 2011.

Abstract:

Invariant-based programming (IBP) is a correct-by-construction programming methodology in which the invariants of a program are developed before the code. We describe here a method for fully automatic translation of an invariant diagram into a functional program, together with the associated consistency, termination and liveness proofs. The generated theorems are the obligations derived using the proof rules of invariant diagrams. The generated program is a refinement of the invariant diagram, and can be directly converted to executable code by Isabelle. This allows verified compilation of invariant diagrams into any of the languages supported by Isabelle code generator.

BibTeX entry:

@INPROCEEDINGS{inpPrBaEr11a,
  title = {Verification and Code Generation for Invariant Diagrams in Isabelle},
  booktitle = {Proceedings of the 23rd Nordic Workshop on Programming Theory},
  author = {Preoteasa, Viorel and Back, Ralph-Johan and Eriksson, Johannes},
  editor = {Petterson, Paul and Seceleanu, Cristina},
  publisher = {Mälardalen Real-Time Research Centre},
  pages = {30--32},
  year = {2011},
}

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

Edit publication