Pubblicazioni

On deciding satisfiability by theorem proving with speculative inferences  (2011)

Autori:
Maria Paola Bonacina; Christopher A. Lynch; Leonardo de Moura
Titolo:
On deciding satisfiability by theorem proving with speculative inferences
Anno:
2011
Tipologia prodotto:
Articolo in Rivista
Tipologia ANVUR:
Articolo su rivista
Nazioni degli autori:
STATI UNITI D'AMERICA; BRASILE; ITALIA
Lingua:
Inglese
Formato:
A Stampa
Referee:
Nome rivista:
Journal of Automated Reasoning
ISSN Rivista:
0168-7433
N° Volume:
47
Numero o Fascicolo:
2
Editore:
Kluwer
Intervallo pagine:
161-189
Parole chiave:
Program checking, Theorem proving, Satisfiability modulo theories, Combination of theories
Breve descrizione dei contenuti:
Applications in software verification often require determining the satisfiability of first-order formulae with respect to background theories. During development, conjectures are usually false. Therefore, it is desirable to have a theorem prover that terminates on satisfiable instances. Satisfiability Modulo Theories (SMT) solvers have proven to be highly scalable, efficient and suitable for integrated theory reasoning. Inference systems with resolution and superposition are strong at reasoning with equalities, universally quantified variables, and Horn clauses. We describe a theorem-proving method that tightly integrates superposition-based inference system and SMT solver. The combination is refutationally complete if background theory symbols only occur in ground formulae, and non-ground clauses are variable-inactive. Termination is enforced by introducing additional axioms as hypotheses. The system detects any unsoundness introduced by these speculative inferences and recovers from it.
Pagina Web:
http://dx.doi.org/10.1007/s10817-010-9213-y
Id prodotto:
59335
Handle IRIS:
11562/344183
depositato il:
24 luglio 2011
ultima modifica:
2 novembre 2016
Citazione bibliografica:
Maria Paola Bonacina; Christopher A. Lynch; Leonardo de Moura, On deciding satisfiability by theorem proving with speculative inferences «Journal of Automated Reasoning» , vol. 47 , n. 22011pp. 161-189

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