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
Artificial intelligence
Pubblicazioni
Titolo Autori Anno
Canonical ground Horn theories Bonacina, Maria Paola; Nachum, Dershowitz 2013
New results on rewrite-based satisfiability procedures Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz 2009
Abstract canonical inference Bonacina, Maria Paola; Nachum, Dershowitz 2007
Rewrite-based satisfiability procedures for recursive data structures Bonacina, Maria Paola; Echenim, Bertrand Mnacho 2007
Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz 2005
On handling distinct objects in the superposition calculus Stephan, Schulz; Bonacina, Maria Paola 2005
Towards a unified model of search in theorem proving: subgoal-reduction strategies Bonacina, Maria Paola 2005

Attività

Strutture

Condividi