Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Proofs and Refutations in Inva...

Proofs and Refutations in Invariant-Based Programming

Johannes Eriksson, Masoumeh Parsa, Ralph-Johan Back, Proofs and Refutations in Invariant-Based Programming. In: Elvira Albert, Emil Sekerinski (Eds.), Proceedings of the 11th International Conference on Integrated Formal Methods (iFM2014), Lecture Notes in Computer Science, 189–204, Springer, 2014.

Abstract:

Invariant-based programming is a correct-by-construction approach to program development in which the invariants of a program are written before the actual code. Socos is an environment for graphically constructing invariant-based programs (as statechart-like diagrams) and verifying their correctness (by invoking an automatic theorem prover). It borrows the specification language, logical framework and proof tactics from the PVS system. In this paper, we describe an extension to Socos for animating invariant-based programs in the logical framework of PVS. An invariant-based program is represented as an abstract datatype encoding the program state coupled a small-step state transition function encoding the operational semantics of the program. Socos visualizes the execution, allowing the user to inspect the current state and identify invalid assertions through test cases. Since programs are executed within the theorem prover framework (rather than translated into another language or compiled to machine code), failed test cases are logically sound refutations of the verification conditions. Invariants not executable in the general (e.g., containing unbounded quantification) can be handled for bounded test cases by introducing custom evaluation functions. While such functions provide no correctness guarantees, they can increase the assurance of a correctness condition before doing the actual proof. We illustrate this workflow through a verification exercise with non-trivial verification conditions, arguing that animation of invariant diagrams serves as an important stepping stone towards a fully verified program.

BibTeX entry:

@INPROCEEDINGS{inpErPaBa14a,
  title = {Proofs and Refutations in Invariant-Based Programming},
  booktitle = {Proceedings of the 11th International Conference on Integrated Formal Methods (iFM2014)},
  author = {Eriksson, Johannes and Parsa, Masoumeh and Back, Ralph-Johan},
  series = {Lecture Notes in Computer Science},
  editor = {Albert, Elvira and Sekerinski, Emil},
  publisher = {Springer},
  pages = {189–204},
  year = {2014},
}

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

Publication Forum rating of this publication: level 1

Edit publication