Generating property-directed potential invariants by quantifier elimination in a k-induction-based framework

This paper addresses the issue of potential invariant generation in the formal analysis of transition systems with k-induction, in the linear real/integer arithmetic fragment. First, quantifier elimination is used to find parameters for generic templates such that the said templates become inductive. Second, a backward analysis, also using quantifier elimination, outputs preimages of the negation of the proof objective, viewed as unauthorized states, or gray states. Two heuristics are proposed to take advantage of this source of information and generate potential invariants: a thorough exploration of the possible partitionings of the gray state space, and an inexact exploration regrouping and over-approximating disjoint areas of the gray state space. Both aim at discovering hidden relations between state variables. K-induction is used to isolate actual invariants and to check if they make the proof objective inductive. These heuristics can be used on the first preimage of the backward exploration, and each time a new one is output, refining the information on the gray states. We show, on examples of interest in the application field of critical embedded systems, that our approach is able to prove properties for which other academic or commercial tools fail. The different methods are introduced as components of a collaborative formal verification framework based on k-induction and are motivated through two examples, one of which was provided by Rockwell Collins.