Maria Paola Bonacina

MariaPaola,  19 ottobre 2012
Qualifica
Professore ordinario
Settore disciplinare
INF/01 - INFORMATICA
Ufficio
Ca' Vignal 2,  Piano 1,  Stanza 73
Telefono
+39 045 802 7046
Fax
+39 045 802 7068
E-mail
mariapaola|bonacina*univr|it <== Sostituire il carattere | con . e il carattere * con @ per avere indirizzo email corretto.
Pagina Web personale
http://profs.sci.univr.it/~bonacina

Orario di ricevimento

mercoledì, Ore 12.00 - 13.30,   Ca' Vignal 2, piano 1, stanza 73

Curriculum

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 della macchina. I campi di applicazione del ragionamento simbolico includono analisi, verifica, e sintesi di sistemi software e hardware, pianificazione, apprendimento automatico, comprensione del linguaggio naturale, matematica al calcolatore, e insegnamento dell'informatica e della matematica. I temi di ricerca di Maria Paola Bonacina includono:
  • procedure di decisione della soddisfacibilità modulo teorie (SMT) basate su deduzione guidata da conflitti, o su inferenze speculative, o su inferenze generiche quali sovrapposizione;
  • dimostrazione automatica di teoremi basata su deduzione guidata da conflitti, o su risoluzione e sovrapposizione, o su tableaux;
  • interpolazione di dimostrazioni per il raffinamento di astrazioni in model checking, o per la generazione di invarianti;
  • parallelizzazione del ragionamento automatico mediante parallelizzazione della ricerca nello spazio delle prove;
  • valutazione ed analisi di strategie per la dimostrazione automatica di teoremi.
Le sue pubblicazioni si collocano prevalentemente sulle riviste internazionali dell'area di ragionamento automatico, computazione simbolica, intelligenza artificiale, e logica computazionale (Journal of Automated Reasoning, ACM Transactions on Computational Logic, Journal of Symbolic Computation, Information and Computation, e altre).
Le conferenze internazionali frequentate includono: International Conference on Automated Deduction (CADE), International Joint Conference on Automated Reasoning (IJCAR), e varie altre conferenze del gruppo della Federated Logic Conference (FLoC).

Insegnamenti

Insegnamenti attivi nel periodo selezionato: 39.
Clicca sull'insegnamento per vedere orari e dettagli del corso.

Corso Nome Crediti totali Online Crediti del docente Moduli svolti da questo docente
Laurea in Informatica Logica [Cognomi A-L] (2017/2018)   6  eLearning
Laurea in Informatica Logica [Cognomi M-Z] (2017/2018)   6  eLearning
Laurea magistrale in Ingegneria e scienze informatiche Ragionamento automatico (2017/2018)   6  eLearning
Laurea in Informatica Logica (2016/2017)   6   
Laurea magistrale in Ingegneria e scienze informatiche Ragionamento automatico (2016/2017)   6   
Laurea magistrale in Ingegneria e scienze informatiche Ragionamento automatico (2014/2015)   6   
Laurea magistrale in Ingegneria e scienze informatiche Verifica automatica di sistemi (2014/2015)   6   
Laurea in Bioinformatica Algoritmi (2013/2014)   12    ALGORITMI PER BIOINFORMATICA
Laurea magistrale in Ingegneria e scienze informatiche Ragionamento automatico (2013/2014)   6   
Laurea magistrale in Ingegneria e scienze informatiche Verifica automatica di programmi (2013/2014)   6   
Laurea in Bioinformatica Algoritmi (2012/2013)   12    ALGORITMI PER BIOINFORMATICA
Laurea magistrale in Ingegneria e scienze informatiche Ragionamento automatico (2012/2013)   6   
Laurea magistrale in Ingegneria e scienze informatiche Verifica automatica di programmi (2012/2013)   6   
Laurea in Bioinformatica Algoritmi (2011/2012)   12    ALGORITMI PER BIOINFORMATICA
Laurea magistrale in Ingegneria e scienze informatiche Ragionamento automatico (2011/2012)   6   
Laurea magistrale in Ingegneria e scienze informatiche Verifica automatica di programmi (2011/2012)   6   
Laurea in Bioinformatica Algoritmi (2010/2011)   12    ALGORITMI PER BIOINFORMATICA
Laurea magistrale in Ingegneria e scienze informatiche Verifica automatica di programmi (2010/2011)   6   
Laurea in Bioinformatica Algoritmi (2009/2010)   12    ALGORITMI PER BIOINFORMATICA
Laurea magistrale in Ingegneria e scienze informatiche Algoritmi (2009/2010)   12    INTELLIGENZA ARTIFICIALE
Laurea magistrale in Ingegneria e scienze informatiche Verifica (2009/2010)   6   
Laurea specialistica in Informatica Deduzione automatica (2008/2009)   5   
Laurea specialistica in Sistemi intelligenti e multimediali Intelligenza artificiale (2008/2009)   5   
Laurea in Informatica (ordinamento fino all'a.a. 2008/09) Linguaggi di programmazione (2008/2009)   5   
Laurea specialistica in Informatica Deduzione automatica (2007/2008)   5   
Laurea specialistica in Sistemi intelligenti e multimediali Intelligenza artificiale (2007/2008)   5   
Laurea in Informatica (ordinamento fino all'a.a. 2008/09) Linguaggi di programmazione (2007/2008)   5   
Laurea specialistica in Informatica Deduzione automatica (2006/2007)   5   
Laurea in Informatica (ordinamento fino all'a.a. 2008/09) Linguaggi di programmazione (2006/2007)   5   
Laurea specialistica in Sistemi intelligenti e multimediali Intelligenza artificiale (2005/2006)   5   
Laurea in Informatica (ordinamento fino all'a.a. 2008/09) Linguaggi di programmazione (2005/2006)   5   
Laurea specialistica in Informatica Deduzione automatica (2004/2005)   5     
Laurea specialistica in Informatica Laboratorio di Informatica (2004/2005)   10     
Laurea in Informatica (ordinamento fino all'a.a. 2008/09) Programmazione [Sezione A] (2004/2005)   12      Teoria
Laurea specialistica in Sistemi intelligenti e multimediali Intelligenza artificiale (2003/2004)   5     
Laurea in Informatica (ordinamento fino all'a.a. 2008/09) Programmazione [Informatica (G-Z)] (2003/2004)   12      Teoria
Laurea specialistica in Sistemi intelligenti e multimediali Intelligenza artificiale (2002/2003)   5     
Laurea in Informatica (ordinamento fino all'a.a. 2008/09) Programmazione [Informatica (G-Z)] (2002/2003)   12      Teoria
Laurea in Informatica (vecchio ordinamento) Laboratorio di informatica (2001/2002)   0     

Attività didattiche avanzate
Nome Online
PhD Course on Special Topics in Artificial Intelligence Model-based Reasoning (32° Ciclo - Dottorato in Informatica)
PhD Course on Special Topics in Artificial Intelligence Model-based Reasoning (31° Ciclo - Dottorato in Informatica)
 

Gruppi di ricerca

ARLette
Ricerca in ragionamento automatico
Logica
Logica in matematica ed informatica.
Competenze
Argomento Descrizione Area di ricerca
Ragionamento automatico Dimostrazione automatica di teoremi; Costruzione automatica di modelli; Ragionamento su programmi; Analisi di strategie di dimostrazione automatica di teoremi; Deduzione automatica distribuita; Strategie di dimostrazione automatica di teoremi: basate su ordinamenti (risoluzione e riscrittura), riduzione a sotto-goal, generazione di istanze; Procedure di decisione per la soddisfacibilità modulo teorie e loro applicazione alla verifica di proprietà di programmi; Sistemi intelligenti
Computing methodologies - Artificial intelligence
Verifica del software Procedure di decisione per la soddisfacibilità modulo teorie e loro applicazione alla verifica di proprietà di programmi; generazione di invarianti mediante dimostrazione di teoremi; generazione di interpolanti mediante dimostrazione di teoremi; raffinamento di astrazioni per model checking o analisi statica mediante dimostrazione di teoremi Informatica teorica
Theory of computation - Logic
Progetti
Titolo Data inizio
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




Organizzazione

Strutture del dipartimento