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.
Type de document :
Communication dans un congrès
8th International Workshop on Satisfiability Modulo Theories, 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00517308
Contributeur : Frédéric Besson <>
Soumis le : mardi 14 septembre 2010 - 10:06:36
Dernière modification le : mardi 16 janvier 2018 - 15:54:15
Document(s) archivé(s) le : mardi 23 octobre 2012 - 16:10:18

Fichier

floating_point_simplex.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00517308, version 1

Citation

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. 2010. 〈inria-00517308〉

Partager

Métriques

Consultations de la notice

206

Téléchargements de fichiers

91