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 assertion-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. © 2014 Springer International Publishing.
CITATION STYLE
Berghammer, R., Höfner, P., & Stucke, I. (2014). Automated verification of relational while-programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8428 LNCS, pp. 173–190). Springer Verlag. https://doi.org/10.1007/978-3-319-06251-8_11
Mendeley helps you to discover research relevant for your work.