Properties of Invariants and Induction Lemmata

Abstract:
Invariants and induction lemmata are of essential importance for many verification procedures. However, even though a given property might be true, it may not be possible to verify it directly by means of induction or invariant rules. Instead, one usually has to strengthen the property so that it becomes inductive, i.e., one has to find a suitable induction lemma. In terms of state transition systems, being inductive means that no transition is leaving the states where the property holds. Recent induction-based methods like property directed reachability (PDR) automatically determine induction lemmata by counterexamples to induction generated for the given property to be verified. For a given property, there are however many suitable invariants or induction lemmata, so that we are interested in the properties of the set of all invariants or induction lemmata. In this paper, we prove that the set of induction lemmata to be used in Park’s fixpoint induction rule for greatest fixpoints is closed both under conjunction and disjunction, and therefore, this set is a lattice. As a consequence, for each greatest fixpoint, there is a weakest and a strongest induction lemma. We furthermore show how these can be computed using quantifier elimination (if the base logic allows this).