Refinement and Term Synthesis in Loop Invariant Generation

Ewen Maclean; Andrew Ireland; Lucas Dixon; Robert Atkey

Refinement and Term Synthesis in Loop Invariant Generation

Ewen Maclean, Andrew Ireland, Lucas Dixon, Robert Atkey

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	WING 2010
Editors	Andrei Voronkov, Laura Kovacs, Nikolaj Bjorner
Publisher	EasyChair
Pages	167-182
Number of pages	16
Publication status	Published - 2012

Publication series

Name	EPiC Series
Publisher	EasyChair
Volume	1

Access to Document

http://www.easychair.org/publications/?page=2127875681

Integration and Interaction of multiple mathematical reasoning processes
Bundy, A. (Principal Investigator), Colton, S. (Sponsor), Aspinall, D. (Co-Investigator (External)), Dennis, L. (Co-Investigator (External)), Fleuriot, J. (Co-Investigator (External)), Georgieva, L. (Co-Investigator (External)), Ireland, A. (Co-Investigator (External)), Jackson, P. (Co-Investigator (External)) & Smaill, A. (Co-Investigator (External))
EPSRC
1/04/07 → 31/03/11
Project: Research

Cite this

@inproceedings{423621c5e5154c1c8d5d2b32e3dfcce3,

title = "Refinement and Term Synthesis in Loop Invariant Generation",

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{\textquoteright}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.",

author = "Ewen Maclean and Andrew Ireland and Lucas Dixon and Robert Atkey",

year = "2012",

language = "English",

series = "EPiC Series",

publisher = "EasyChair",

pages = "167--182",

editor = "Andrei Voronkov and Laura Kovacs and Nikolaj Bjorner",

booktitle = "WING 2010",

}

TY - GEN

T1 - Refinement and Term Synthesis in Loop Invariant Generation

AU - Maclean, Ewen

AU - Ireland, Andrew

AU - Dixon, Lucas

AU - Atkey, Robert

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

M3 - Conference contribution

T3 - EPiC Series

SP - 167

EP - 182

BT - WING 2010

A2 - Voronkov, Andrei

A2 - Kovacs, Laura

A2 - Bjorner, Nikolaj

PB - EasyChair

ER -

Refinement and Term Synthesis in Loop Invariant Generation

Abstract

Publication series

Access to Document

Fingerprint

Projects

Integration and Interaction of multiple mathematical reasoning processes

Cite this