On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

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

(1)
1

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.
Fichier principal
Vignette du fichier
floating_point_simplex.pdf (177.15 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00517308 , version 1 (14-09-2010)

Identifiers

  • HAL Id : inria-00517308 , version 1

Cite

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⟩
153 View
69 Download

Share

Gmail Facebook Twitter LinkedIn More