Below I provide the list of my main software developments. Links to other scripts and smaller software libraries are available either from the Publications tab or directly in the main text of my research articles.
TSSOS is a Julia package implementing a new moment-SOS hierarchy, for solving large-scale sparse polynomial optimization problems. Its novelty is to exploit simultaneously correlative sparsity and term sparsity, by combining advantages of two existing frameworks for sparse polynomial optimization. The former is due to Waki et al. while the latter was initially proposed by Wang et al. and later exploited in the TSSOS hierarchy. In doing so we obtain a two-level hierarchy of semidefinite programming relaxations with (i), the crucial property to involve quasi block-diagonal matrices and (ii), the guarantee of convergence to the global optimum. TSSOS can handle several large-scale instances of the celebrated Max-Cut problem and the important industrial optimal power flow problem, involving up to several thousands of variables and ten thousands of constraints.
The Maple package RealCertify tackles the problem of deciding the non-negativity of rational polynomials over semi-algebraic domains defined by polynomial constraints with rational coefficients. This is done by computing sum of squares certificates of non-negativity for inputs where such certificates hold over the rational numbers. It can be applied to numerous problems coming from engineering sciences, program verification and cyber-physical systems. It is based on hybrid symbolic-numeric algorithms based on semi-definite programming.
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).
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.
TSSOS: a sparse polynomial optimization tool based on block moment-SOS hierarchies.
See the dedicated webpage.TSSOS is a Julia package implementing a new moment-SOS hierarchy, for solving large-scale sparse polynomial optimization problems. Its novelty is to exploit simultaneously correlative sparsity and term sparsity, by combining advantages of two existing frameworks for sparse polynomial optimization. The former is due to Waki et al. while the latter was initially proposed by Wang et al. and later exploited in the TSSOS hierarchy. In doing so we obtain a two-level hierarchy of semidefinite programming relaxations with (i), the crucial property to involve quasi block-diagonal matrices and (ii), the guarantee of convergence to the global optimum. TSSOS can handle several large-scale instances of the celebrated Max-Cut problem and the important industrial optimal power flow problem, involving up to several thousands of variables and ten thousands of constraints.
RealCertify: a Maple package for certifying non-negativity.
See the dedicated webpage.The Maple package RealCertify tackles the problem of deciding the non-negativity of rational polynomials over semi-algebraic domains defined by polynomial constraints with rational coefficients. This is done by computing sum of squares certificates of non-negativity for inputs where such certificates hold over the rational numbers. It can be applied to numerous problems coming from engineering sciences, program verification and cyber-physical systems. It is based on hybrid symbolic-numeric algorithms based on semi-definite programming.
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).
NLCertify: a tool for formal nonlinear optimization.
See the dedicated webpage.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.