Skip to Main content Skip to Navigation
Conference papers

On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver

Frédéric Besson 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Off-the-shelf linear programming (LP) solvers trade soundness for speed: for efficiency, the arithmetic is not exact rational arithmetic but floating-point arithmetic. As a side-effect the results come without any formal guarantee and cannot be directly used for decid- ing linear arithmetic. In this work we explain how to design a sound procedure for linear arithmetic built upon an inexact floating-point LP solver. Our approach relies on linear programming duality to instruct a black-box off-the-shelf LP solver to output, when the problem is not satisfiable, an untrusted proof certificate. We present a heuristic post- processing of the certificate which accommodates for certain numeric inaccuracies. Upon success it returns a provably correct proof witness that can be independently checked. Our preliminary results are promising. For a benchmark suite extracted from SMT verification problems the floating-point LP solver returns a result for which proof witnesses are successfully and efficiently generated.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Frédéric Besson Connect in order to contact the contributor
Submitted on : Tuesday, September 14, 2010 - 10:06:36 AM
Last modification on : Thursday, January 20, 2022 - 4:20:09 PM
Long-term archiving on: : Tuesday, October 23, 2012 - 4:10:18 PM


Files produced by the author(s)


  • HAL Id : inria-00517308, version 1


Frédéric Besson. On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver. 8th International Workshop on Satisfiability Modulo Theories, 2010, Edinburgh, United Kingdom. ⟨inria-00517308⟩



Les métriques sont temporairement indisponibles