• 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 Myréen, Testing and Verifying Invariant Based Programs in the SOCOS Environment. TUCS Technical Reports 797, Turku Centre for Computer Science, 2006.

Abstract:

SOCOS is a prototype tool for constructing programs and reasoning about their correctness. It supports the invariants-first programming methodology by providing a diagrammatic environment for specification, implementation and execution of procedural programs. Invariants, pre- and postconditions can be evaluated at runtime, following the Design by Contract paradigm. SOCOS can also generate correctness conditions for static program verification 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 PVS.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tBaErMy06a,
  title = {Testing and Verifying Invariant Based Programs in the SOCOS Environment},
  author = {Back, Ralph-Johan and Eriksson, Johannes and Myréen, Magnus},
  number = {797},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2006},
  keywords = {Invariant based programming, verification, SOCOS},
  ISBN = {952-12-1835-5},
}

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

Edit publication