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.