Trustworthy Systems

Tool-based verification of a relational vertex coloring program

Authors

Rudolf Berghammer, Peter Hoefner and Insa Stucke

Christian-Albrechts-Universität zu Kiel

NICTA

UNSW

Abstract

We present different approaches of using a special purpose computer algebra system and theorem provers in software verification. To this end, we first develop a purely algebraic while-program for computing a vertex coloring of an undirected (loop-free) graph. For showing its correctness, we then combine the well-known assertion-based verification method with relation-algebraic calculations. Based on this, we show how automatically to test loop-invariants by means of the RelView tool and also compare the usage of three different theorem provers in respect to the verification of the proof obligations: the automated theorem prover Prover9 and the two proof assistants Coq and Isabelle/HOL. As a result, we illustrate that algebraic abstraction yields verification tasks that can easily be verified with off-the-shelf theorem provers, but also reveal some shortcomings and difficulties with theorem provers that are nowadays available.

BibTeX Entry

  @inproceedings{Berghammer_HS_15,
    address          = {Braga},
    author           = {Berghammer, Rudolf and H\"ofner, Peter and Stucke, Insa},
    booktitle        = {International Conference on Relational and Algebraic Methods in Computer Science},
    month            = sep,
    pages            = {18},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8899.pdf},
    title            = {Tool-Based Verification of a Relational Vertex Coloring Program},
    year             = {2015}
  }

Download