Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT

Pascal Fontaine 1, 2, 3, 4 Mizuhito Ogawa 5 Thomas Sturm 2, 4, 3 Van Khanh To 6 Xuan Tung Vu 5
1 UL - Université de Lorraine
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
4 CNRS - Centre National de la Recherche Scientifique
5 JAIST - Japan Advanced Institute of Science and Technology
6 VNU - Vietnam National University [Hanoï]
Abstract : We report on a prototypical tool for Satisfiability Modulo Theory solving for quantifier-free formulas in Non-linear Real Arithmetic or, more precisely, real closed fields, which uses a computer algebra system as the main component. This is complemented with two heuristic techniques, also stemming from computer algebra, viz. interval constraint propagation and subtropical satisfiability. Our key idea is to make optimal use of existing knowledge and work in the symbolic computation community, reusing available methods and implementations to the most possible extent. Experimental results show that our approach is surprisingly efficient in practice.
Type de document :
Communication dans un congrès
SC-square 2018 - Third International Workshop on Satisfiability Checking and Symbolic Computation, Jul 2018, Oxford, United Kingdom
Liste complète des métadonnées
https://hal.inria.fr/hal-01946733
Contributeur : Pascal Fontaine <>
Soumis le : jeudi 6 décembre 2018 - 12:35:39
Dernière modification le : lundi 10 décembre 2018 - 15:03:50

Fichier

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

Identifiants

  • HAL Id : hal-01946733, version 1

Collections

UNIV-LORRAINE | LORIA-FM | LORIA | INRIA

Citation

Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Van Khanh To, Xuan Tung Vu. Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT. SC-square 2018 - Third International Workshop on Satisfiability Checking and Symbolic Computation, Jul 2018, Oxford, United Kingdom. 〈hal-01946733〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

17

Téléchargements de fichiers

36

Contact


archive-ouverte@inria.fr