NLCertify: A tool for formal nonlinear optimization
File(s)
Accepted version
Author(s)
Magron, V
Type
Conference Paper
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.
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.
Date Issued
2014-05-22
Date Acceptance
2014-08-05
Citation
Proceedings of the 4th International Congress of Mathematical Software, 2014, 8592, pp.315-320
ISBN
978-3-662-44199-2
Publisher
Springer
Start Page
315
End Page
320
Journal / Book Title
Proceedings of the 4th International Congress of Mathematical Software
Volume
8592
Copyright Statement
© 2014, Springer-Verlag Berlin Heidelberg. The final publication is available at Springer via https://dx.doi.org/10.1007/978-3-662-44199-2_49
Source
4th International Congress of Mathematical Software (ICMS 2014)
Subjects
Formal Nonlinear Optimization
Hybrid Symbolic-Numeric Certification
Proof Assistant
Sparse SOS
Maxplus Approximation
Publication Status
Published
Start Date
2014-08-05
Coverage Spatial
Seoul, South Korea