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

Data inizio
21 novembre 2003
Durata (mesi) 
24
Dipartimenti
Informatica
Responsabili (o referenti locali)
Bonacina Maria Paola
URL
http://profs.sci.univr.it/~bonacina/prin2003.html
Parole chiave
Ragionamento automatico, procedure di decisione, model checking

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".

Enti finanziatori:

Ministero dell'Istruzione dell'Università e della Ricerca
Finanziamento: assegnato e gestito dal dipartimento

Partecipanti al progetto

Maria Paola Bonacina
Professore ordinario

Collaboratori esterni

Massimo Benerecetti
Università degli Studi di Napoli Federico II
Alessandro Armando
Università degli Studi di Genova
Silvio Ranise
INRIA Lorraine Ricercatore
Aree di ricerca coinvolte dal progetto
Sistemi intelligenti
Computing methodologies - Artificial intelligence
Pubblicazioni
Titolo Autori Anno
Canonical ground Horn theories Maria Paola Bonacina; Nachum Dershowitz 2013
New results on rewrite-based satisfiability procedures Alessandro Armando; Maria Paola Bonacina; Silvio Ranise; Stephan Schulz 2009
Canonical inference for implicational systems Maria Paola Bonacina; Nachum Dershowitz 2008
Abstract canonical inference Maria Paola Bonacina; Nachum Dershowitz 2007
Rewrite-based satisfiability procedures for recursive data structures Maria Paola Bonacina; Mnacho Echenim 2007
Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures Alessandro Armando; Maria Paola Bonacina; Silvio Ranise; Stephan Schulz 2005
On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal Alessandro Armando; Maria Paola Bonacina; Silvio Ranise; Stephan Schulz 2005
On handling distinct objects in the superposition calculus Stephan Schulz; Maria Paola Bonacina 2005
Towards a unified model of search in theorem proving: subgoal-reduction strategies Maria Paola Bonacina 2005

Attività

Strutture