Pubblicazioni

Theory decision by decomposition  (2010)

Autori:
Maria Paola Bonacina; Mnacho Echenim
Titolo:
Theory decision by decomposition
Anno:
2010
Tipologia prodotto:
Articolo in Rivista
Tipologia ANVUR:
Articolo su rivista
Lingua:
Inglese
Formato:
A Stampa
Referee:
Nome rivista:
Journal of Symbolic Computation
ISSN Rivista:
0747-7171
N° Volume:
45
Numero o Fascicolo:
2
Editore:
Elsevier
Intervallo pagine:
229-260
Breve descrizione dei contenuti:
The topic of this article is decision procedures for satisfiability modulo theories (SMT) of arbitrary quantifier-free formul\ae. We propose an approach that decomposes the formula in such a way that its definitional part, including the theory, can be compiled by a rewrite-based first-order theorem prover, and the residual problem can be decided by an SMT-solver, based on the Davis-Putnam-Logemann-Loveland procedure. The resulting decision by stages mechanism may unite the complementary strengths of first-order provers and SMT-solvers. We demonstrate its practicality by giving decision procedures for the theories of records, integer offsets and arrays, with or without extensionality, and for combinations including such theories.
Pagina Web:
http://dx.doi.org/10.1016/j.jsc.2008.10.008; http://profs.sci.univr.it/~bonacina/
Id prodotto:
47518
Handle IRIS:
11562/323520
depositato il:
15 marzo 2012
ultima modifica:
22 maggio 2017
Citazione bibliografica:
Maria Paola Bonacina; Mnacho Echenim, Theory decision by decomposition «Journal of Symbolic Computation» , vol. 45 , n. 22010pp. 229-260

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

Progetti Collegati
Titolo Dipartimento Responsabili
Integrazione di metodi di ragionamento automatico nel model checking: verifica formale automatica di sistemi di grande scala e a stati infiniti - Progetto ed integrazione di macchine di prova per l'analisi di programmi (PRIN 2007) Dipartimento Informatica Maria Paola Bonacina
<<indietro

Attività

Strutture