Sintesi di procedure di decisione basate sulla deduzione con applicazioni all'analisi formale automatica di programmi (PRIN 2003)

Sintesi di procedure di decisione basate sulla deduzione con applicazioni all'analisi formale automatica di programmi -- Sintesi di procedure di soddisfacibilità da strategie di dimostrazione automatica Poichè un numero crescente di applicazioni critiche dipende dall'affidabilità dei programmi, la validazione del software ha bisogno di tecniche flessibili, potenti ed efficaci relativamente al costo, che tuttavia siano facili da usare. Questo progetto risponde a questi bisogni sviluppando ed applicando tecnologie deduttive ad alte prestazioni per sostenere l'analisi automatica e formale del software. L'approccio adottato è quello di combinare i vantaggi del ragionamento logico altamente espressivo e di procedure di decisione specializzate per produrre tecniche efficienti e "push-button".