ProgCertSOS

Certified program analysis using Sum-of-Squares (SOS) programming

ProgCertSOS is a tool to check whether a given property holds for the values taken by the variables of a program.
The tool uses abstract template domains.
ProgCertSOS takes as input one-loop programs with conditional branches, nondeterministic initial values and the desired property, e.g.
while true
if r(x) >= 0
x = T1(x);
else
x = T2(x);
end
end

All the input (T1, T2, r) are Yalmip polynomials.

This tool implements the Sum-of-Squares (SOS)-based techniques described in the article "Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization" (available on https://hal.inria.fr/hal-01134816)