ProgCertSOS
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
Platform Compatibility
Windows macOS LinuxCategories
Tags
Community Treasure Hunt
Find the treasures in MATLAB Central and discover how the community can help you!
Start Hunting!Discover Live Editor
Create scripts with code, output, and formatted text in a single executable document.