Probabilistic Guarantees for Practical LIA Loop Invariant Automation

TL;DR

The paper tackles invariant synthesis for safety-critical software by introducing DLIA$^2$, a probabilistic, data-driven approach that combines simulated annealing, SMT verification, and computational geometry to guarantee convergence for single-loop $LIA$ CHC systems. It advances the field by establishing termination and success guarantees via $bepsilon$-nets over ellipsoids and a cost function based on a polytope-set distance, while leveraging parallel SA and iterated implication pairs to improve local progress. Empirical results on SV-COMP benchmarks show competitive performance against state-of-the-art tools like GSpacer, with notable strength on benchmarks featuring complex transition relations. The work provides a principled framework for probabilistic invariant search that can be extended to broader theories such as Linear Real Arithmetic, enabling robust data-driven verification of real-world programs.

Abstract

Despite the crucial need for formal safety and security verification of programs, discovering loop invariants remains a significant challenge. Static analysis is a primary technique for inferring loop invariants but often relies on substantial assumptions about underlying theories. Data-driven methods supported by dynamic analysis and machine learning algorithms have shown impressive performance in inferring loop invariants for some challenging programs. However, state-of-the-art data-driven techniques do not offer theoretical guarantees for finding loop invariants. We present a novel technique that leverages the simulated annealing (SA) search algorithm combined with SMT solvers and computational geometry to provide probabilistic guarantees for inferring loop invariants using data-driven methods. Our approach enhances the SA search with real analysis to define the search space and employs parallelism to increase the probability of success. To ensure the convergence of our algorithm, we adapt e-nets, a key concept from computational geometry. Our tool, DLIA2, implements these algorithms and demonstrates competitive performance against state-of-the-art techniques. We also identify a subclass of programs, on which we outperform the current state-of-the-art tool GSpacer.

Figures (25)

• Figure 1: An example C program.
• Figure 2: Diagram showing input-output behavior of DS and SA Loops of DLIA$^2$.
• Figure 3: In the examples shown, the ground positive states are represented by all the lattice points within the dark green triangle, while the green dots indicate the sampled positive points. The left example demonstrates a poor approximation of $+_g$ as the sampling is concentrated near a single vertex of the triangle. In contrast, the right example provides a better approximation by distributing the sampled points more evenly across the triangle.
• Figure 4: In the above figure, we aim to probe an SMT solver for distinct LIA models within the black triangle. Figure (a) illustrates the plot of the first model, which is a vertex of the triangle. To obtain a second distinct model, we add the constraint $( (x,y) \neq (x_f, y_f) ) \equiv ( x < x_f \lor x > x_f \lor y < y_f \lor y > y_f ),$ where $(x_f, y_f)$ are the coordinates of the first model. This constraint modifies the sampling space, with the new boundaries drawn in red. Sampling from this space results in a new vertex as a model, but unfortunately, it is very close to the first model, as depicted in Figure (b). Finally, Figure (c) shows the result of sampling many distinct counterexamples from the black triangle.
• Figure 5: Iterations of DS Loop show the challenge of satisfying implication pairs and the benefit of ICE pairs.

Theorems & Definitions (22)

• definition 1
• definition 2
• definition 3
• theorem 1
• definition 4
• definition 5
• definition 6
• definition 7
• lemma 1
• theorem 2