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 OCAMLlibraries that produce nonnegativity certificates for the function over the box, which can be ultimately proved correct inside the COQ proof assistant. © 2014 Springer-Verlag.
CITATION STYLE
Magron, V. (2014). NLCertify: A tool for formal nonlinear optimization. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8592 LNCS, pp. 315–320). Springer Verlag. https://doi.org/10.1007/978-3-662-44199-2_49
Mendeley helps you to discover research relevant for your work.