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)

Data inizio
22 settembre 2008
Durata (mesi) 
24
Dipartimenti
Informatica
Responsabili (o referenti locali)
Bonacina Maria Paola
URL
http://profs.sci.univr.it/~bonacina/prin2007.html
Parole chiave
Ragionamento automatico; analisi di programmi; procedure di decisione per soddisfacibilità modulo teorie; dimostrazione automatica di teoremi basata su riscrittura; generazione automatica di modelli

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 Poichè il software è ovunque, l'impatto economico degli errori nel software non può essere sovrastimato. Il costo degli errori potrebbe essere ridotto in modo significativo, mediante tecniche che permettano di scoprire e rimuovere prima e più efficacemente i difetti. L'importanza del problema impone di investigare tecniche completamente automatiche. I successi del model checking di hardware e protocolli suggeriscono di investigare il model checking di software. Tuttavia, questo è considerevolmente più difficile, perchè il software significa sistemi con infiniti stati. La complessità si attacca con l'astrazione: se un pezzo di software è troppo complesso, se ne analizza una versione astratta, più semplice dell'originale. Tuttavia, un errore trovato nel modello astratto non è necessariamente un errore nel programma concreto. Per colmare la distanza tra l'astratto e il concreto, occorre il ragionamento automatico. La corrispondenza tra errore nel modello ed errore nel programma concreto si riduce a un problema di soddisfacibilità, la cui prova si usa per raffinare l'astrazione, se si è scoperto un errore spurio. Il contributo centrale di questo progetto è la definizione, progetto ed implementazione di procedure di decisione per la soddisfacibilità, che siano efficienti, espressive e tali da scalare in prestazioni.

Enti finanziatori:

Ministero dell'Istruzione dell'Università e della Ricerca
Finanziamento: assegnato e gestito dal dipartimento
Programma: COFIN - Progetti di Ricerca di Interesse Nazionale

Partecipanti al progetto

Maria Paola Bonacina
Professore ordinario
Aree di ricerca coinvolte dal progetto
Sistemi intelligenti
Computing methodologies - Artificial intelligence
Pubblicazioni
Titolo Autori Anno
Interpolation systems for ground proofs in automated deduction: a survey Maria Paola Bonacina; Moa Johansson 2015
On interpolation in automated theorem proving Maria Paola Bonacina; Moa Johansson 2015
Canonical ground Horn theories Maria Paola Bonacina; Nachum Dershowitz 2013
On deciding satisfiability by theorem proving with speculative inferences Maria Paola Bonacina; Christopher A. Lynch; Leonardo de Moura 2011
On interpolation in decision procedures Maria Paola Bonacina; Moa Johansson 2011
Towards interpolation in an SMT solver with integrated superposition Maria Paola Bonacina; Moa Johansson 2011
On theorem proving for program checking - Historical perspective and recent developments Maria Paola Bonacina 2010
Theory decision by decomposition Maria Paola Bonacina; Mnacho Echenim 2010
On deciding satisfiability by DPLL(Gamma+T) and unsound theorem proving Maria Paola Bonacina; Christopher A. Lynch; Leonardo de Moura 2009

Attività

Strutture