Automatic Decidability: A Schematic Calculus for Theories with Counting Operators

Elena Tushkanova 1 Christophe Ringeissen 1 Alain Giorgetti 1 Olga Kouchnarenko 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 : Many verification problems can be reduced to a satisfiability problem modulo theories. For building satisfiability procedures the rewriting-based approach uses a general calculus for equational reasoning named paramodulation. Schematic paramodulation, in turn, provides means to reason on the derivations computed by paramodulation. Until now, schematic paramodulation was only studied for standard paramodulation. We present a schematic paramodulation calculus modulo a fragment of arithmetics, namely the theory of Integer Offsets. This new schematic calculus is used to prove the decidability of the satisfiability problem for some theories equipped with counting operators. We illustrate our theoretical contribution on theories representing extensions of classical data structures, e.g., lists and records. An implementation within the rewriting-based Maude system constitutes a practical contribution. It enables automatic decidability proofs for theories of practical use.
Type de document :
Communication dans un congrès
RTA - 24th International Conference on Rewriting Techniques and Applications - 2013, Jun 2013, Eindhoven, Netherlands. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 21, pp.303-318, 2013, LIPIcs. 〈10.4230/LIPIcs.RTA.2013.303〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00878657
Contributeur : Christophe Ringeissen <>
Soumis le : mercredi 30 octobre 2013 - 14:32:25
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

Citation

Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, Olga Kouchnarenko. Automatic Decidability: A Schematic Calculus for Theories with Counting Operators. RTA - 24th International Conference on Rewriting Techniques and Applications - 2013, Jun 2013, Eindhoven, Netherlands. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 21, pp.303-318, 2013, LIPIcs. 〈10.4230/LIPIcs.RTA.2013.303〉. 〈hal-00878657〉

Partager

Métriques

Consultations de la notice

319