Generating Property-Directed Potential Invariants By Backward Analysis
This work addresses lemma generation for formal verification in critical avionics systems, representing an incremental improvement with domain-specific applications.
The paper tackles the problem of generating lemmas for k-induction-based formal verification of transition systems in linear real/integer arithmetic by using backward analysis with quantifier elimination to identify unauthorized states and applying heuristics to discover potential invariants. It shows that this approach outperforms other academic and commercial tools in the context of critical avionics embedded systems.
This paper addresses the issue of lemma generation in a k-induction-based formal analysis of transition systems, in the linear real/integer arithmetic fragment. A backward analysis, powered by quantifier elimination, is used to output 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. First, a thorough exploration of the possible partitionings of the gray state space discovers new relations between state variables, representing potential invariants. Second, an inexact exploration regroups and over-approximates disjoint areas of the gray state space, also to discover new relations between state variables. k-induction is used to isolate the invariants and check if they strengthen the proof objective. 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. In our context of critical avionics embedded systems, we show that our approach is able to outperform other academic or commercial tools on examples of interest in our application field. The method is introduced and motivated through two main examples, one of which was provided by Rockwell Collins, in a collaborative formal verification framework.