NLCertify: a tool for formal nonlinear optimization

DOI10.1007/978-3-662-44199-2_49MaRDI QIDQ2879141zbMATH OpenOpenAlexFDO

Authors Victor Magron

Publication date 8 September 2014

Published in Mathematical Software – ICMS 2014 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1405.5668

zbMATH Keywords

formal nonlinear optimizationhybrid symbolic-numeric certificationmax-plus approximationproof assistantsparse SOS

Mathematics Subject Classification ID

Packaged methods for numerical algorithms (65Y15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Software, source code, etc. for problems pertaining to operations research and mathematical programming (90-04) Tropical optimization (e.g., max-plus optimization) (90C24) Nonlinear programming (90C30)

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 and a transcendental multivariate function as input, NLCertify provides OCaml libraries that produce nonnegativity certificates for the function over the box, which can be ultimately proved correct inside the Coq proof assistant.

Recommendations

• Formal Proofs for Nonlinear Optimization
• Certification of bounds of non-linear functions: the templates method
• Certification of real inequalities: templates and sums of squares
• {\textsc{RealCertify}}: a Maple package for certifying non-negativity
• Dynamics of a parametrically excited system with two forcing terms

Cited in

(7)

• NLCertify
• Certification of real inequalities: templates and sums of squares
• Gposolver: a Matlab/C++ toolbox for global polynomial optimization
• Certification of bounds of non-linear functions: the templates method
• {\textsc{RealCertify}}: a Maple package for certifying non-negativity
• Dynamics of a parametrically excited system with two forcing terms
• Formal Proofs for Nonlinear Optimization

Describes a project that uses

Uses Software

• Coq
• SparsePOP
• GloptiPoly
• YALMIP
• OCaml
• Sollya

This page was built for publication: NLCertify: a tool for formal nonlinear optimization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879141)