Automated verification of relational while-programs
Authors
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, month = apr, paperurl = {https://ts.data61.csiro.au/publications/nicta_full_text/7613.pdf}, booktitle = {International Conference on Relational and Algebraic Methods in Computer Science}, author = {Berghammer, Rudolf and H\"ofner, Peter and Stucke, Insa}, year = {2014}, pages = {16}, title = {Automated Verification of Relational While-Programs}, address = {Marienstatt im Westerwald, Germany} }