Skip to main content

TS

Automated verification of relational while-programs

Authors

Rudolf Berghammer, Peter Hoefner and Insa Stucke

Christian-Albrechts-Universität zu Kiel

NICTA

UNSW

Abstract

Software verification is essential for safety-critical systems. In this paper, we illustrate that some verification tasks can be done fully automatically. We show how to automatically verify imperative programs for relation-based discrete structures by combining relation algebra and the well-known invariant-based verification method with automated theorem proving. We present two examples in detail: a relational program for determining the reflexive-transitive closure and a topological sorting algorithm. We also treat the automatic verification of the equivalence of common-logical and relation-algebraic specifications.

BibTeX Entry

  @inproceedings{Berghammer_HS_14,
    author           = {Berghammer, Rudolf and Höfner, Peter and Stucke, Insa},
    month            = apr,
    year             = {2014},
    title            = {Automated Verification of Relational While-Programs},
    booktitle        = {14th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2014)},
    pages            = {16},
    address          = {Marienstatt im Westerwald, Germany}
  }

Download

Served by Apache on Linux on seL4.