"ReLIC: Reduced Logic Inference for Composition" for Quantifier Elimination based Compositional Reasoning and Verification

TL;DR

This paper introduces ReLIC, a novel approach leveraging quantifier elimination for compositional reasoning and verification, enabling efficient derivation of system properties and integration with model-checking tools.

Contribution

The paper presents a new framework for quantifier elimination-based compositional reasoning, extending it to time-dependent properties and integrating it with model-checking tools and industrial verification workflows.

Findings

ReLIC effectively derives the strongest system properties from component properties.

Integration with Redlog and JKind solves non-linear problems SMT tools struggle with.

Applicable to industrial V&V for Simulink models and DNNs.

Abstract

The paper presents our research on quantifier elimination (QE) for compositional reasoning and verification. For compositional reasoning, QE provides the foundation of our approach, serving as the calculus for composition to derive the strongest system-property in a single step, from the given component atomic-properties and their interconnection relation. We first developed this framework for time-independent properties, and later extended it to time-dependent property composition. The extension requires, in addition, shifting the given properties along time to span the time horizon of interest, he least of which for the strongest system-property is no more than the total time horizons of the component level atomic-properties. The system-initial-condition is also composed from atomic-initial-conditions of the components the same way. It is used to verify a desired system-level property, alongside the derived strongest system-property, by way of induction. Our composition approach is uniform regardless of the composition types (cascade/parallel/feedback) for both time-dependent and time-independent properties. We developed a new prototype verifier named ReLIC (Reduced Logic Inference for Composition) that implements our above approaches. We demonstrated it through several illustrative and practical examples. Further, we advanced the $k$-induction based model-checking with QE capabilities, by formulating its base and inductive steps into QE problems where all the variables are universally quantified. Our integration of the QE solver Redlog with the $k$-induction based model-checking tool JKind, shows the successful solving of a non-linear problem that the SMT capable JKind failed to resolve. Finally, we also showcase the recent adoption of our approaches within an industrial V\&V tool suite for augmented static analysis of Simulink models and Deep Neural Networks (DNNs).