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)

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.