Maria Paola Bonacina

MariaPaola,  19 ottobre 2012
Qualifica
Professore ordinario
Settore disciplinare
INF/01 - INFORMATICA
Settore di Ricerca (ERC)
PE6_7 - Artificial intelligence, intelligent systems, multi agent systems

PE6_4 - Theoretical computer science, formal methods, and quantum computing

Ufficio
Ca' Vignal 2,  Piano 1,  Stanza 73
Telefono
+39 045 802 7046
E-mail
mariapaola|bonacina*univr|it <== Sostituire il carattere | con . e il carattere * con @ per avere indirizzo email corretto.
Pagina Web personale
https://mariapaola.github.io/

Orario di ricevimento

martedì, Ore 12.30 - 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 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).

Insegnamenti

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

Corso Nome Crediti totali Online Crediti del docente Moduli svolti da questo docente
Laurea magistrale in Artificial Intelligence Planning and Automated Reasoning (2023/2024)   12  eLearning AUTOMATED REASONING
PLANNING
Laurea magistrale in Ingegneria e scienze informatiche Verifica automatica di sistemi (2023/2024)   6  eLearning
Laurea magistrale in Artificial Intelligence Planning and Automated Reasoning (2022/2023)   12  eLearning AUTOMATED REASONING
PLANNING
Laurea magistrale in Ingegneria e scienze informatiche Verifica automatica di sistemi (2022/2023)   6  eLearning
Laurea magistrale in Ingegneria e scienze informatiche Fondamenti di linguaggi di programmazione e specifica (2020/2021)   12  eLearning (Teoria)
Dottorato in Informatica Attività didattica dottorato (2019/2020)   50  eLearning
Laurea in Informatica Logica [Matricole dispari] (2019/2020)   6  eLearning
Laurea magistrale in Ingegneria e scienze informatiche Ragionamento automatico (2019/2020)   6  eLearning
Laurea in Informatica Logica [Matricole pari] (2018/2019)   6  eLearning
Laurea magistrale in Ingegneria e scienze informatiche Ragionamento automatico (2018/2019)   6  eLearning
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     

Per la comunità studentesca

Se sei già iscritta/o a un corso di studio, puoi consultare tutti gli avvisi relativi al tuo corso di studi nella tua area riservata MyUnivr.
In questo portale potrai visualizzare informazioni, risorse e servizi utili che riguardano la tua carriera universitaria (libretto online, gestione della carriera Esse3, corsi e-learning, email istituzionale, modulistica di segreteria, procedure amministrative, ecc.).
Entra in MyUnivr con le tue credenziali GIA: solo così potrai ricevere notifica di tutti gli avvisi dei tuoi docenti e della tua segreteria via mail e a breve anche tramite l'app Univr.

MyUnivr
 

Gruppi di ricerca

ARLette - Laboratorio di Ragionamento Automatico
Il gruppo svolge ricerche in Ragionamento Automatico: dimostrazione di teoremi, procedure di decisione, soddisfacibilità modulo assegnamenti, costruzione di modelli, riscrittura, e applicazioni.
Intelligenza Artificiale (IA)
Il gruppo svolge ricerche in Intelligenza Artificiale: Ragionamento Automatico, Algoritmi di Ricerca, Rappresentazione della Conoscenza, Apprendimento Automatico, Sistemi Multi-Agenti e applicazioni.
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
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
Logic
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




Organizzazione

Strutture del dipartimento

Condividi