Pubblicazioni

New results on rewrite-based satisfiability procedures  (2009)

Autori:
Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz
Titolo:
New results on rewrite-based satisfiability procedures
Anno:
2009
Tipologia prodotto:
Articolo in Rivista
Tipologia ANVUR:
Articolo su rivista
Lingua:
Inglese
Formato:
A Stampa
Referee:
Nome rivista:
ACM Transactions on Computational Logic
ISSN Rivista:
1529-3785
N° Volume:
1
Numero o Fascicolo:
10
Editore:
ACM
Intervallo pagine:
129-179
Parole chiave:
Decision procedures; satisfiability modulo theories; combination of theories; inference; superposition; rewriting; termination; scalability
Breve descrizione dei contenuti:
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 a theory T. If a sound and complete inference system for first-order logic is guaranteed to terminate on T-satisfiability problems, a 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 combinations 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.
Pagina Web:
http://doi.acm.org/10.1145/1459010.1459014
https://mariapaola.github.io/
Id prodotto:
33854
Handle IRIS:
11562/225588
depositato il:
15 marzo 2012
ultima modifica:
15 settembre 2023
Citazione bibliografica:
Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz, New results on rewrite-based satisfiability procedures «ACM Transactions on Computational Logic» , vol. 1 , n. 102009pp. 129-179

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo IRIS

Progetti Collegati
Titolo Dipartimento Responsabili
Sintesi di procedure di decisione basate sulla deduzione con applicazioni all'analisi formale automatica di programmi (PRIN 2003) Dipartimento Informatica Maria Paola Bonacina
<<indietro

Attività

Strutture

Condividi