Satisfiability Procedures for Combination of Theories Sharing Integer Offsets

Enrica Nicolini 1 Christophe Ringeissen 1 Michael Rusinowitch 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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a novel technique to combine satisfiability procedures for theories that model some data-structures and that share the integer offsets. This procedure extends the Nelson-Oppen approach to a family of non-disjoint theories that have practical interest in verification. The result is derived by showing that the considered theories satisfy the hypotheses of a general result on non-disjoint combination. In particular, the capability of computing logical consequences over the shared signature is ensured in a non trivial way by devising a suitable complete superposition calculus.
Type de document :
Communication dans un congrès
Stefan Kowalewski and Anna Philippou. 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS 2009, Mar 2009, York, United Kingdom. Springer, 5505, pp.428-442, 2009, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00427870
Contributeur : Christophe Ringeissen <>
Soumis le : mercredi 28 octobre 2009 - 17:17:18
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

  • HAL Id : inria-00427870, version 1

Citation

Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch. Satisfiability Procedures for Combination of Theories Sharing Integer Offsets. Stefan Kowalewski and Anna Philippou. 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS 2009, Mar 2009, York, United Kingdom. Springer, 5505, pp.428-442, 2009, Lecture Notes in Computer Science. 〈inria-00427870〉

Partager

Métriques

Consultations de la notice

151