Efficient formal verification of bounds of linear programs

DOI10.1007/978-3-642-22673-1_9MaRDI QIDQ5200112zbMATH OpenOpenAlexFDO

Authors Alexey Solovyev, Thomas C. Hales

Publication date 29 July 2011

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

Full work available at URL https://doi.org/10.1007/978-3-642-22673-1_9

Mathematics Subject Classification ID

Numerical mathematical programming methods (65K05) Linear programming (90C05)

Recommendations

• Theorem Proving in Higher Order Logics
• Formal Proofs for Nonlinear Optimization
• scientific article; zbMATH DE number 1614683
• A formal proof of the Kepler conjecture
• Flyspecking Flyspeck

Cites work

• A proof of the Kepler conjecture
• Flyspeck II: The basic linear programs
• Formal proof - the four color theorem
• scientific article; zbMATH DE number 1042857 (Why is no real title available?)
• Linear Programs for the Kepler Conjecture

Cited in

(10)

• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• scientific article; zbMATH DE number 1614683 (Why is no real title available?)
• Affine arithmetic and applications to real-number proving
• A new PCP outer verifier with applications to homogeneous linear equations and max-bisection
• Formal Proofs for Nonlinear Optimization
• A formal proof of the Kepler conjecture
• Theorem Proving in Higher Order Logics
• Logic Based Program Synthesis and Transformation
• Accelerating and verifying constant-time modular inversion
• On verified numerical computations in convex programming

Describes a project that uses

Uses Software

• GLPK
• Flyspeck
• kepler98
• HOL Light

This page was built for publication: Efficient formal verification of bounds of linear programs

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