Generating Property-Directed Potential Invariants By Backward Analysis

TL;DR

This paper introduces a backward analysis method using quantifier elimination to generate property-directed invariants for transition systems, improving lemma generation in k-induction-based formal verification, especially in avionics systems.

Contribution

It presents novel heuristics leveraging backward analysis to discover invariants and strengthen proofs, outperforming existing tools in critical avionics applications.

Findings

Outperforms other tools on avionics examples

Effective in discovering invariants through backward analysis

Enhances lemma generation in formal verification

Abstract

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.