Generating Loop Invariants for Program Verification by Transformation

Loop invariants play a central role in the verification of imperative programs. However, finding these invariants is often a difficult and time-consuming task for the programmer. We have previously shown how program transformation can be used to facilitate the verification of functional programs, bu...

Full description

Bibliographic Details
Main Author: G. W. Hamilton
Format: Article
Language:English
Published: Open Publishing Association 2017-08-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1708.07223v1