Automatic Decidability for Theories Modulo Integer Offsets

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, 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 superposition. Schematic superposition, in turn, provides a mean to reason on the derivations computed by superposition. Until now, schematic superposition was only studied for standard superposition. We present a schematic superposition 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 extending Integer Offsets. We illustrate our theoretical contribution on theories representing extensions of classical data structures, e.g., lists and records. An implementation in the rewriting-based Maude system constitutes a practical contribution. It enables automatic decidability proofs for theories of practical use.
Type de document :
Rapport
[Research Report] RR-8139, INRIA. 2012, pp.20
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00753896
Contributeur : Christophe Ringeissen <>
Soumis le : lundi 19 novembre 2012 - 17:56:07
Dernière modification le : jeudi 11 janvier 2018 - 01:58:29
Document(s) archivé(s) le : jeudi 21 février 2013 - 11:41:43

Fichier

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

Identifiants

  • HAL Id : hal-00753896, version 1

Citation

Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, Olga Kouchnarenko. Automatic Decidability for Theories Modulo Integer Offsets. [Research Report] RR-8139, INRIA. 2012, pp.20. 〈hal-00753896〉

Partager

Métriques

Consultations de la notice

327

Téléchargements de fichiers

148