Publications

Theory decision by decomposition  (2010)

Authors:
Maria Paola Bonacina; Mnacho Echenim
Title:
Theory decision by decomposition
Year:
2010
Type of item:
Articolo in Rivista
Tipologia ANVUR:
Articolo su rivista
Language:
Inglese
Format:
A Stampa
Referee:
Name of journal:
Journal of Symbolic Computation
ISSN of journal:
0747-7171
N° Volume:
45
Number or Folder:
2
:
Elsevier
Page numbers:
229-260
Short description of contents:
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.
Web page:
http://dx.doi.org/10.1016/j.jsc.2008.10.008; http://profs.sci.univr.it/~bonacina/
Product ID:
47518
Handle IRIS:
11562/323520
Deposited On:
March 15, 2012
Last Modified:
May 22, 2017
Bibliographic citation:
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

Related projects
Title Department Managers
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) Department Informatica Maria Paola Bonacina
<<back

Activities

Research facilities