Synthesizing invariants by solving solvable loops

TL;DR

This paper introduces a new method for automatically generating loop invariants in programs with polynomial and non-deterministic assignments, utilizing eigenvector generation and polynomial optimization, implemented in the open-source tool Pilat.

Contribution

It presents a novel approach combining eigenvector analysis and polynomial optimization to synthesize invariants for complex loops, advancing automated program verification.

Findings

Successfully handles polynomial and non-deterministic assignments

Implemented in the open-source tool Pilat

Enhances automatic invariant generation capabilities

Abstract

When proving invariance properties of a program, we face two problems. The first problem is related to the necessity of proving tautologies of considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes a new method for the automatic generation of loop invariants that handles polynomial and non deterministic assignments. This technique is based on the eigenvector generation for a given linear transformation and on the polynomial optimization problem, which we implemented in the open-source tool Pilat.