ProgCertSOS

Certified program analysis using Sum-of-Squares (SOS) programming
244 Downloads
Updated Fri, 27 Mar 2015 11:56:04 +0000

View License

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)

Cite As

Victor Magron (2024). ProgCertSOS (https://www.mathworks.com/matlabcentral/fileexchange/48210-progcertsos), MATLAB Central File Exchange. Retrieved .

MATLAB Release Compatibility
Created with R2014b
Compatible with any release
Platform Compatibility
Windows macOS Linux

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!
Version Published Release Notes
1.3.0.0

Update preprint link

1.2.0.0

Fixed description

1.1.0.0

Fixed typo in the program description

1.0.0.0