Verifying Nonlinear Real Formulas Via Sums of Squares

DOI10.1007/978-3-540-74591-4_9zbMath1144.68357OpenAlexW1534704094MaRDI QIDQ3523169

No author found.

Publication date: 2 September 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74591-4_9

Mathematics Subject Classification ID

Related Items (24)

Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ A heuristic prover for real inequalities ⋮ ATLAS: automated amortised complexity analysis of self-adjusting data structures ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Computing sum of squares decompositions with rational coefficients ⋮ HOL Light: An Overview ⋮ Proving tight bounds on univariate expressions with elementary functions in Coq ⋮ Duality of sum of nonnegative circuit polynomials and optimal SONC bounds ⋮ Amortized Complexity Verified ⋮ Mathematics and the formal turn ⋮ Efficient and accurate computation of upper bounds of approximation errors ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ DSOS and SDSOS Optimization: More Tractable Alternatives to Sum of Squares and Semidefinite Optimization ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ Proving Bounds on Real-Valued Functions with Computations ⋮ A Short Presentation of Coq ⋮ Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials ⋮ Amortized complexity verified ⋮ A revision of the proof of the Kepler conjecture ⋮ Real World Verification ⋮ Validating numerical semidefinite programming solvers for polynomial invariants ⋮ On the Generation of Positivstellensatz Witnesses in Degenerate Cases ⋮ Combined Decision Techniques for the Existential Theory of the Reals ⋮ Formalization of Bernstein polynomials and applications to global optimization

Uses Software

• CSDP
• HOL Light

This page was built for publication: Verifying Nonlinear Real Formulas Via Sums of Squares