NLCertify: a tool for formal nonlinear optimization.


See the dedicated webpage.

Abstract: NLCertify is a software package for handling formal certification of nonlinear inequalities involving transcendental multivariate functions. The tool exploits sparse semialgebraic optimization techniques with approximation methods for transcendental functions, as well as formal features. Given a box K and a function f as input, NLCertify provides OCaml libraries that produce nonnegativity certificates for f over K, which can be ultimately proved correct inside the Coq proof assistant. One specific challenge of the field of formal nonlinear reasoning is to develop adaptive techniques to produce certificates with a reduced complexity.

The software first builds the abstract syntax tree t of f. The leaves of t are semialgebraic functions obtained by composition of polynomials with some basic operations (including the square root, sup, inf, +, x, -, /, etc). The other nodes can be either univariate transcendental functions (arctan, cos, exp, etc) or basic operations. NLCertify approximates t with means of semialgebraic estimators and provides lower and upper bounds of t over K. When t represents a polynomial, the tool computes lower and upper bounds of t using a hierarchy of semidefinite (SDP) relaxations, via an interface with the external SDPA solver. The extension to the semialgebraic case is straightforward through the implementation of the Lasserre-Putinar lifting-strategy. The user can choose to approximate transcendental functions with best uniform (or minimax) polynomials as well as maxplus estimators. Univariate minimax polynomials are provided using an interface with the Sollya environment, in which an iterative algorithm designed by Remez is implemented. Alternatively, the maxplus approach builds lower (resp. upper) estimators using concave maxima (resp. convex infima) of quadratic forms. In this way, NLCertify computes certified global estimators from approximations of primitive functions by induction over the syntax tree t.

These various approximation and optimization algorithms are placed in a unified framework extending to about 15000 lines of OCaml code and 3600 lines of Coq code. The NLCertify package solves successfully non-trivial inequalities from the Flyspeck project (essentially tight inequalities, involving both semialgebraic and transcendental expressions of 6~12 variables) as well as significant global optimization benchmarks.

ParetoImageSDP: approximations of Pareto curves and images of semialgebraic sets.


See the dedicated webpage.

ParetoImageSDP is a set of libraries using the Yalmip and Gloptipoly toolboxes for MATLAB. It provides functions to compute semidefinite approximations of:

1) Pareto curves implementing the three methods described in: Victor Magron, Didier Henrion and Jean-Bernard Lasserre "Approximating Pareto curves using semidefinite relaxations" (on the arxiv).

2) Images of semialgebraic sets under polynomial applications implementing the two methods described in Victor Magron, Didier Henrion and Jean-Bernard Lasserre "Semidefinite approximations of projections and polynomial images of semialgebraic sets" (on Optimization Online).

ProgCertSOS: certified program analysis using sum-of-squares (SOS) programming.


See the dedicated webpage.

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 a given property $\kappa$ to show. A simple example is the following program:

while true
  if $r(x) \geq 0$
   $x = T_1(x)$;
  else
   $x = T_2(x)$;
  end
end

with the property $\kappa = 1 - \|x\|^2$ (all reachable values lie in the unit sphere).

This tool implements SOS-based techniques described in the article "Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization" hal-01134816.

Real2Float: A tool for Certified Roundoff Error Bounds Using SDP.


See the dedicated webpage.

Real2Float is a set of libraries to analyze floating-point errors of nonlinear programs with semidefinite programming. The tool requires OCaml, SDPA and Coq (optional).