Finding polynomial loop invariants for probabilistic programs

TL;DR

This paper introduces a new method for synthesizing polynomial loop invariants in probabilistic programs using sum-of-squares and semidefinite programming, offering a semi-complete and efficient approach.

Contribution

It presents an alternative to multivariate Lagrange interpolation by fixing a polynomial template and applying sum-of-squares techniques for invariant synthesis.

Findings

Method is semi-complete and guarantees a solution if one exists.

Approach is efficient and effective on experimental benchmarks.

Utilizes semidefinite programming for invariant synthesis.

Abstract

Quantitative loop invariants are an essential element in the verification of probabilistic programs. Recently, multivariate Lagrange interpolation has been applied to synthesizing polynomial invariants. In this paper, we propose an alternative approach. First, we fix a polynomial template as a candidate of a loop invariant. Using Stengle's Positivstellensatz and a transformation to a sum-of-squares problem, we find sufficient conditions on the coefficients. Then, we solve a semidefinite programming feasibility problem to synthesize the loop invariants. If the semidefinite program is unfeasible, we backtrack after increasing the degree of the template. Our approach is semi-complete in the sense that it will always lead us to a feasible solution if one exists and numerical errors are small. Experimental results show the efficiency of our approach.