Satisfiability Modulo Bounded Checking

Simon Cruanes 1
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We describe a new approach to find models for a computational higher-order logic with datatypes. The goal is to find counterexamples for conjectures stated in proof assistants. The technique builds on narrowing [14] but relies on a tight integration with a SAT solver to analyze conflicts precisely, eliminate sets of choices that lead to failures, and sometimes prove unsatisfiability. The architecture is reminiscent of that of an SMT solver. We present the rules of the calculus, an implementation, and some promising experimental results.
Type de document :
Communication dans un congrès
International Conference on Automated Deduction (CADE), Aug 2017, Gothenburg, Sweden. 26, pp.114-129, 2017, 〈10.1007/978-3-319-63046-5_8〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01572531
Contributeur : Simon Cruanes <>
Soumis le : mardi 8 août 2017 - 16:08:43
Dernière modification le : mercredi 9 août 2017 - 01:08:19

Fichier

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

Identifiants

Collections

Citation

Simon Cruanes. Satisfiability Modulo Bounded Checking. International Conference on Automated Deduction (CADE), Aug 2017, Gothenburg, Sweden. 26, pp.114-129, 2017, 〈10.1007/978-3-319-63046-5_8〉. 〈hal-01572531〉

Partager

Métriques

Consultations de
la notice

148

Téléchargements du document

17