Affine Disjunctive Invariant Generation with Farkas' Lemma

TL;DR

This paper introduces a new automated method for generating affine disjunctive invariants in loop programs using Farkas' Lemma, improving the analysis of complex loop behaviors.

Contribution

It combines Farkas' Lemma with control flow transformation and invariant propagation, and extends to nested loops, addressing previous infeasibility issues.

Findings

Successfully generated tight invariants for over 100 affine loops

Demonstrated effectiveness on SV-COMP 2023 benchmarks

Improved invariant computation efficiency

Abstract

In the verification of loop programs, disjunctive invariants are essential to capture complex loop dynamics such as phase and mode changes. In this work, we develop a novel approach for the automated generation of affine disjunctive invariants for affine while loops via Farkas' Lemma, a fundamental theorem on linear inequalities. Our main contributions are two-fold. First, we combine Farkas' Lemma with a succinct control flow transformation to derive disjunctive invariants from the conditional branches in the loop. Second, we propose an invariant propagation technique that minimizes the invariant computation effort by propagating previously solved invariants to yet unsolved locations as much as possible. Furthermore, we resolve the infeasibility checking in the application of Farkas' Lemma which has not been addressed previously, and extend our approach to nested loops via loop summary. Experimental evaluation over more than 100 affine while loops (mostly from SV-COMP 2023) demonstrates that our approach is promising to generate tight linear invariants over affine programs.