Projects per year
We present a technique for refining incorrect or insufficiently strong loop invariants in correctness proofs for imperative programs. We rely on previous work  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.
|Title of host publication||WING 2010|
|Editors||Andrei Voronkov, Laura Kovacs, Nikolaj Bjorner|
|Number of pages||16|
|Publication status||Published - 2012|