Polynomial Template Generation using Sum-of-Squares Programming

TL;DR

This paper introduces a method for generating polynomial templates for program analysis by leveraging sum-of-squares programming, enabling the verification of properties in polynomial arithmetic programs.

Contribution

It formalizes the concept of well-representative template bases and connects template generation with solving SOS-based systems of inequalities.

Findings

Effective polynomial templates can be generated for program invariants.

The SOS hierarchy provides certificates for property verification.

Application demonstrated on nontrivial polynomial programs.

Abstract

Template abstract domains allow to express more interesting properties than classical abstract domains. However, template generation is a challenging problem when one uses template abstract domains for program analysis. In this paper, we relate template generation with the program properties that we want to prove. We focus on one-loop programs with nested conditional branches. We formally define the notion of well-representative template basis with respect to such programs and a given property. The definition relies on the fact that template abstract domains produce inductive invariants. We show that these invariants can be obtained by solving certain systems of functional inequalities. Then, such systems can be strengthened using a hierarchy of sum-of-squares (SOS) problems when we consider programs written in polynomial arithmetic. Each step of the SOS hierarchy can possibly provide a solution which in turn yields an invariant together with a certificate that the desired property holds. The interest of this approach is illustrated on nontrivial program examples in polynomial arithmetic.