Edinburgh Research Explorer

Refinement and Term Synthesis in Loop Invariant Generation

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publicationWING 2010
EditorsAndrei Voronkov, Laura Kovacs, Nikolaj Bjorner
PublisherEasyChair
Pages167-182
Number of pages16
StatePublished - 2012

Publication series

NameEPiC Series
PublisherEasyChair
Volume1

Abstract

We present a technique for refining incorrect or insufficiently strong loop invariants in correctness proofs for imperative programs. We rely on previous work [16] in combining program analysis and Proof Planning, and exploit IsaPlanner’s use of meta-variables and goal-naming to generate correct loop invariants. We present a simple example in detail and show how this scales to more complex problems.

ID: 6362286