Automated Verification of Relational While-Programs

Select |




Print


Berghammer, Rudolf; Höfner, Peter; Stucke, Insa

Berghammer, Rudolf; Höfner, Peter; Stucke, Insa


2014-04-27


Conference Material


14th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2014)


Marienstatt im Westerwald, Germany


16


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.


http://mathcs.chapman.edu/ramics2014/


nicta:7613


Berghammer, Rudolf; Höfner, Peter; Stucke, Insa. Automated Verification of Relational While-Programs. In: 14th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2014); Marienstatt im Westerwald, Germany. 2014-04-27. 16.



Loading citation data...

Citation counts
(Requires subscription to view)