Maria Paola Bonacina

Curriculum

•   Curriculum vitae - EN   (pdf, en, 276 KB, 28/09/21)
•   Curriculum vitae - IT   (pdf, it, 276 KB, 28/09/21)

Maria Paola Bonacina svolge ricerche sul ragionamento simbolico, una branca dell'intelligenza artificiale dedicata a rendere i computer capaci di ragionamento, non necessariamente imitando forme di intelligenza naturale, ma piuttosto a modo loro. Maria Paola si occupa prevalentemente di ragionamento automatico, dove l'enfasi è sulla capacità della macchina di produrre soluzioni anche senza una frequente interazione con l'utente, e di ragionamento logico-deduttivo, dove la logica è il linguaggio di rappresentazione e la deduzione è il principale meccanismo computazionale. I campi di applicazione del ragionamento automatico includono l'analisi, verifica, e sintesi di sistemi software e hardware, la pianificazione, la comprensione del linguaggio naturale, la matematica al calcolatore, e l'insegnamento dell'informatica e della matematica. Il ragionamento automatico è collegato a parecchi altri campi dell'informatica quali la computazione simbolica e l'apprendimento automatico. I temi di ricerca di Maria Paola Bonacina includono:

• Dimostrazione automatica di teoremi basata su deduzione guidata da conflitti (SGGS), o su strategie basate su ordinamenti (risoluzione e sovrapposizione), o su tableaux;
• Procedure di decisione della soddisfacibilità modulo teorie ed assegnamenti (SMA) basate su deduzione guidata da conflitti (CDSAT), inferenze speculative, o metodi di inferenza generali per la dimostrazione automatica;
• Interpolazione di dimostrazioni per la generazione di invarianti o il raffinamento di astrazioni in model checking;
• Parallelizzazione del ragionamento automatico mediante parallelizzazione della ricerca nello spazio delle inferenze;
• Valutazione ed analisi di strategie per la dimostrazione automatica di teoremi.

Maria Paola pubblica prevalentemente su riviste internazionali che coprono il ragionamento automatico, la computazione simbolica, l'intelligenza artificiale, e la logica computazionale, quali Journal of Automated Reasoning, ACM Transactions on Computational Logic, Journal of Logic and Computation, Journal of Symbolic Computation, Information and Computation. Maria Paola partecipa regolarmente a conferenze internazionali quali la International Conference on Automated Deduction (CADE), la International Joint Conference on Automated Reasoning (IJCAR), e varie altre conferenze specialmente tra quelle del gruppo della Federated Logic Conference (FLoC).

 

Progetti

Titolo	Data inizio
SGGS: algoritmi e implementazione	23/03/17
Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato)	18/02/13
Analisi, verifica e sintesi di sistemi software/hardware mediante l'impiego sinergico di interpretazione astratta e ragionamento automatico (PRIN 2010-11 non finanziato)	01/06/12
Combinazione di analisi e sintesi di programmi: co-generazione di astrazioni e raffinamenti per l'analisi e la sintesi di programmi (PRIN 2009 valutato positivamente ma non finanziato)	15/07/11
Rich-model toolkit: an infrastructure for reliable computer systems (EU COST Action IC0109) 2009-2013	30/10/09
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)	22/09/08
Metodi di ragionamento automatico per l'analisi di hardware e software: progetto, integrazione, applicazione - Grandi macchine di prova come piccole macchine di prova: progetto, integrazione ed applicazione all'analisi di programmi (PRIN 2006 valutato positivamente ma non finanziato)	09/02/07
Sintesi di procedure di decisione basate sulla deduzione con applicazioni all'analisi formale automatica di programmi (PRIN 2003)	21/11/03

---

Maria Paola Bonacina

Carica	Organo collegiale
componente	Consiglio del Dipartimento di Informatica - Dipartimento Informatica