Probabilistic Guarantees for Practical LIA Loop Invariant Automation

TL;DR

This paper introduces DLIA2, a novel data-driven approach using simulated annealing, SMT solvers, and computational geometry to probabilistically guarantee loop invariant inference, outperforming existing methods in certain program subclasses.

Contribution

The paper presents a new technique combining simulated annealing, real analysis, and e-nets to provide probabilistic guarantees for loop invariant inference with improved performance.

Findings

DLIA2 demonstrates competitive performance against state-of-the-art tools.

The approach outperforms GSpacer on a specific subclass of programs.

Probabilistic guarantees are achieved through novel algorithmic integration.

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.