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

Verifying Invariant Based Programs in the SOCOS Environment

Ralph-Johan Back, Johannes Eriksson, Magnus Myreen, Verifying Invariant Based Programs in the SOCOS Environment. In: Paul Boca, Jonathan Bowen, David Duce (Eds.), Teaching Formal Methods: Practice and Experience, Electronic Workshops in Computing (eWiC), 0, BCS, 2006.

Abstract:

An invariant based program is a state transition diagram consisting
of nested situations (predicates over program variables) and transitions
between situations (predicate transformers). Reasoning about correctness
is performed in a local fashion by examining each situation at a time
and proving that the situation is satisfied for all possible executions.
Since the invariants are in place from the beginning and the verification
conditions are easily extracted from the diagram there is no need
for complicated proof rules, making invariant diagrams a suitable
notation for introducing formal verification to students and programmers.
Our preliminary experience from using invariant diagrams in the classroom
has prompted the need for a tool to support the method: we introduce
here SOCOS, an environment for invariant based programming. SOCOS
generates correctness conditions based on weakest precondition semantics,
and 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:

Abstract in PDF-format

BibTeX entry:

@INPROCEEDINGS{inpBaErMy06a,
  title = {Verifying Invariant Based Programs in the SOCOS Environment},
  booktitle = {Teaching Formal Methods: Practice and Experience},
  author = {Back, Ralph-Johan and Eriksson, Johannes and Myreen, Magnus},
  series = {Electronic Workshops in Computing (eWiC)},
  editor = {Boca, Paul and Bowen, Jonathan and Duce, David},
  publisher = {BCS},
  pages = {0},
  year = {2006},
}

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

Edit publication