Maria Paola Bonacina

MariaPaola,  October 19, 2012
Position
Full Professor
Academic sector
INF/01 - INFORMATICS
Office
Ca' Vignal 2,  Floor 1,  Room 73
Telephone
+39 045 802 7046
Fax
+39 045 802 7068
E-mail
mariapaola|bonacina*univr|it <== Replace | with . and * with @ to have the right email address.
Personal web page
http://profs.sci.univr.it/~bonacina

Office Hours

Wednesday, Hours 12:30 PM - 2:00 PM,   Ca' Vignal 2, floor 1, room 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).

Modules

Modules running in the period selected: 39.
Click on the module to see the timetable and course details.

Course Name Total credits Online Teacher credits Modules offered by this teacher
Master's degree in Computer Science and Engineering Automated reasoning (2017/2018)   6  eLearning
Bachelor's degree in Computer Science Logic [Cognomi A-L] (2017/2018)   6  eLearning
Bachelor's degree in Computer Science Logic [Cognomi M-Z] (2017/2018)   6  eLearning
Master's degree in Computer Science and Engineering Automated reasoning (2016/2017)   6   
Bachelor's degree in Computer Science Logic (2016/2017)   6   
Master's degree in Computer Science and Engineering Automated reasoning (2014/2015)   6   
Master's degree in Computer Science and Engineering Automated System Verification (2014/2015)   6   
Bachelor's degree in Bioinformatics Algorithms for Bioinformatics (2013/2014)   12    ALGORITMI PER BIOINFORMATICA
Master's degree in Computer Science and Engineering Automated program verification (2013/2014)   6   
Master's degree in Computer Science and Engineering Automated reasoning (2013/2014)   6   
Bachelor's degree in Bioinformatics Algorithms for Bioinformatics (2012/2013)   12    ALGORITMI PER BIOINFORMATICA
Master's degree in Computer Science and Engineering Automated program verification (2012/2013)   6   
Master's degree in Computer Science and Engineering Automated reasoning (2012/2013)   6   
Bachelor's degree in Bioinformatics Algorithms for Bioinformatics (2011/2012)   12    ALGORITMI PER BIOINFORMATICA
Master's degree in Computer Science and Engineering Automated program verification (2011/2012)   6   
Master's degree in Computer Science and Engineering Automated reasoning (2011/2012)   6   
Bachelor's degree in Bioinformatics Algorithms for Bioinformatics (2010/2011)   12    ALGORITMI PER BIOINFORMATICA
Master's degree in Computer Science and Engineering Automated program verification (2010/2011)   6   
Bachelor's degree in Bioinformatics Algorithms for Bioinformatics (2009/2010)   12    ALGORITMI PER BIOINFORMATICA
Master's degree in Computer Science and Engineering Algorithms for Bioinformatics (2009/2010)   12    INTELLIGENZA ARTIFICIALE
Master's degree in Computer Science and Engineering Verifica (2009/2010)   6   
Masters in Intelligent and Multimedia Systems Artificial Intelligence (2008/2009)   5   
Masters in Computer Science Automated Deduction (2008/2009)   5   
Bachelor in Computer Science (until 2008-2009 academic year) Programming Languages (2008/2009)   5   
Masters in Intelligent and Multimedia Systems Artificial Intelligence (2007/2008)   5   
Masters in Computer Science Automated Deduction (2007/2008)   5   
Bachelor in Computer Science (until 2008-2009 academic year) Programming Languages (2007/2008)   5   
Masters in Computer Science Automated Deduction (2006/2007)   5   
Bachelor in Computer Science (until 2008-2009 academic year) Programming Languages (2006/2007)   5   
Masters in Intelligent and Multimedia Systems Artificial Intelligence (2005/2006)   5   
Bachelor in Computer Science (until 2008-2009 academic year) Programming Languages (2005/2006)   5   
Masters in Computer Science Automated Deduction (2004/2005)   5     
Masters in Computer Science Computing workshop (2004/2005)   10     
Bachelor in Computer Science (until 2008-2009 academic year) Introduction to Programming [Sezione A] (2004/2005)   12      Teoria
Masters in Intelligent and Multimedia Systems Artificial Intelligence (2003/2004)   5     
Bachelor in Computer Science (until 2008-2009 academic year) Introduction to Programming [Informatica (G-Z)] (2003/2004)   12      Teoria
Masters in Intelligent and Multimedia Systems Artificial Intelligence (2002/2003)   5     
Bachelor in Computer Science (until 2008-2009 academic year) Introduction to Programming [Informatica (G-Z)] (2002/2003)   12      Teoria
Bachelor in Computer Science (old system) Computing workshop (2001/2002)   0     

Advanced teaching activities
Name Online
PhD Course on Special Topics in Artificial Intelligence Model-based Reasoning (32° Ciclo - PhD in Computer Science)
PhD Course on Special Topics in Artificial Intelligence Model-based Reasoning (31° Ciclo - PhD in Computer Science)
 

Research groups

ARLette
Research in automated reasoning
Logica
Logica in matematica ed informatica.
Skills
Topic Description Research area
Automated Reasoning Automated theorem proving; Automated model building; Reasoning about programs; Strategy analysis; Distributed automated deduction; Theorem proving strategies: ordering-based strategies (resolution and rewriting), subgoal-reduction strategies, instance-based strategies; Decision procedures for satisfiability modulo theories and their application to check program properties Sistemi intelligenti
Computing methodologies - Artificial intelligence
Software Verification Decision procedures for satisfiability modulo theories and their application to check program properties; invariant generation by theorem proving; interpolating theorem proving; abstraction refinement for either model checking or static analysis by theorem proving Informatica teorica
Theory of computation - Logic
Projects
Title Starting date
Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato) 2/18/13
Analysis, verification and synthesis of hw/sw systems through synergies of abstract interpretation and automated reasoning 6/1/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) 7/15/11
Rich-model toolkit: an infrastructure for reliable computer systems 10/30/09
Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems - Design and integration of proof engines for program analysis 9/22/08
Automated reasoning methods for hardware and software analysis: design, integration and application 2/9/07
Synthesis of deduction-based decision procedures with applications to the automatic formal analysis of software -- Synthesis of satisfiability procedures from theorem-proving strategies 11/21/03