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

Testing and Verifying Invariant Based Programs in the SOCOS Environment

Ralph-Johan Back, Johannes Eriksson, Magnus Myreen, Testing and Verifying Invariant Based Programs in the SOCOS Environment. In: Yuri Gurevich, Bertrand Meyer (Eds.), Tests And Proofs (First International Conference, TAP 2007, Zurich, Switzerland), Lecture Notes in Computer Science 4454, 61–78, Springer, 2007.

http://dx.doi.org/10.1007/978-3-540-73770-4_4

Abstract:

SOCOS is a prototype tool for constructing programs and reasoning about their correctness. It supports the invariant based programming methodology by providing a diagrammatic environment for specication, implementation, verication and execution of procedural programs. Invariants and contracts (pre- and postconditions) can be evaluated at runtime, following the Design by Contract paradigm. SOCOS can also generate correctness conditions for static program verication based on the weakest precondition semantics of statements. To verify the program the user can attempt to automatically discharge these conditions using the Simplify theorem prover; conditions which were not automatically discharged can be proved interactively in the PVS theorem prover.

Files:

Full publication in PDF-format

BibTeX entry:

@INPROCEEDINGS{inpBaErMy07a,
  title = {Testing and Verifying Invariant Based Programs in the SOCOS Environment},
  booktitle = {Tests And Proofs (First International Conference, TAP 2007, Zurich, Switzerland)},
  author = {Back, Ralph-Johan and Eriksson, Johannes and Myreen, Magnus},
  volume = {4454},
  series = {Lecture Notes in Computer Science},
  editor = {Gurevich, Yuri and Meyer, Bertrand},
  publisher = {Springer},
  pages = {61–78},
  year = {2007},
  keywords = {Invariant based programming, program verification, static checking},
}

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

Publication Forum rating of this publication: level 1

Edit publication