On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

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

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Identifiants

  • HAL Id : inria-00517308 , version 1

Citer

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⟩
171 Consultations
73 Téléchargements

Partager

Gmail Facebook X LinkedIn More