New results on rewrite-based satisfiability procedures

Alessandro Armando 1 Maria Paola Bonacina 2 Silvio Ranise 3 Stephan Schulz 2
3 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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literals in theory T. If a sound and complete inference system for first-order logic is guaranteed to terminate on T-satisfiability problems, any theorem-proving strategy with that system and a fair search plan is a T-satisfiability procedure. We prove termination of a rewrite-based first-order engine on the theories of records, integer offsets, integer offsets modulo and lists. We give a modularity theorem stating sufficient conditions for termination on a combination of theories, given termination on each. The above theories, as well as others, satisfy these conditions. We introduce several sets of benchmarks on these theories and their combinations, including both parametric synthetic benchmarks to test scalability, and real-world problems to test performances on huge sets of literals. We compare the rewrite-based theorem prover E with the validity checkers CVC and CVC Lite. Contrary to the folklore that a general-purpose prover cannot compete with reasoners with built-in theories, the experiments are overall favorable to the theorem prover, showing that not only the rewriting approach is elegant and conceptually simple, but has important practical implications.
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2009, 10 (1), Article 4, 51 p. 〈10.1145/1459010.1459014〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00576862
Contributeur : Christophe Ringeissen <>
Soumis le : mardi 15 mars 2011 - 14:58:28
Dernière modification le : mardi 13 mars 2018 - 14:24:05

Lien texte intégral

Identifiants

Citation

Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic, Association for Computing Machinery, 2009, 10 (1), Article 4, 51 p. 〈10.1145/1459010.1459014〉. 〈inria-00576862〉

Partager

Métriques

Consultations de la notice

122