8665 articles  [version française]

hal-00753896, version 1

Automatic Decidability for Theories Modulo Integer Offsets

Elena Tushkanova a1, Christophe Ringeissen (, http://www.loria.fr/~ringeiss) 1, Alain Giorgetti () a1, Olga Kouchnarenko () 1

N° RR-8139 (2012)

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.

  • a –  Université de Franche-Comté
  • 1:  CASSIS (INRIA Nancy - Grand Est / LORIA / LIFC)
  • Université de Lorraine – Université de Franche-Comté – CNRS : FRE2661 – INRIA
  • Domain : Computer Science/Logic in Computer Science
  • Internal note : RR-8139
 
  • hal-00753896, version 1
  • oai:hal.inria.fr:hal-00753896
  • From: 
  • Submitted on: Monday, 19 November 2012 17:56:07
  • Updated on: Friday, 23 November 2012 15:48:49