A rule-based system for automatic decidability and combinability

Elena Tushkanova 1, 2 Alain Giorgetti 1, 2 Christophe Ringeissen 1 Olga Kouchnarenko 2, 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This paper deals with decision procedures specified by using a superposition calculus which is an inference system at the core of all equational theorem provers. This calculus is refutation complete: it provides a semi-decision procedure that halts on unsatisfiable inputs but may diverge on satisfiable ones. Fortunately, it may also terminate for some theories of interest in verification, and thus it becomes a decision procedure. To reason on the superposition calculus, a schematic superposition calculus has been developed to build the schematic form of the saturations allowing to automatically prove decidability of single theories and of their combinations. This paper presents a rule-based logical framework and a tool implementing a complete many-sorted schematic superposition calculus for arbitrary theories. By providing results for unit theories, arbitrary theories, and also for theories with counting operators, we show that this tool is very useful to derive decidability and combinability of theories of practical interest in verification.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2015, Selected Papers from the Ninth International Workshop on Rewriting Logic and its Applications (WRLA 2012), 99, pp.3-23. 〈10.1016/j.scico.2014.02.005〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01102883
Contributeur : Christophe Ringeissen <>
Soumis le : jeudi 15 janvier 2015 - 17:35:36
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : samedi 12 septembre 2015 - 06:28:30

Fichier

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

Identifiants

Citation

Elena Tushkanova, Alain Giorgetti, Christophe Ringeissen, Olga Kouchnarenko. A rule-based system for automatic decidability and combinability. Science of Computer Programming, Elsevier, 2015, Selected Papers from the Ninth International Workshop on Rewriting Logic and its Applications (WRLA 2012), 99, pp.3-23. 〈10.1016/j.scico.2014.02.005〉. 〈hal-01102883〉

Partager

Métriques

Consultations de la notice

335

Téléchargements de fichiers

135