Refinement and Term Synthesis in Loop Invariant Generation

Ewen Maclean, Andrew Ireland, Lucas Dixon, Robert Atkey

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

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationWING 2010
EditorsAndrei Voronkov, Laura Kovacs, Nikolaj Bjorner
Number of pages16
Publication statusPublished - 2012

Publication series

NameEPiC Series


Dive into the research topics of 'Refinement and Term Synthesis in Loop Invariant Generation'. Together they form a unique fingerprint.

Cite this