Maria Paola Bonacina

MariaPaola,  October 19, 2012
Position
Full Professor
Academic sector
INF/01 - INFORMATICS
Research sector (ERC)
PE6_7 - Artificial intelligence, intelligent systems, multi agent systems

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

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

Tuesday, Hours 11:00 AM - 12:00 PM,   Ca' Vignal 2, Floor 1, room 73

Curriculum

Maria Paola Bonacina conducts research in symbolic reasoning, a field of artificial intelligence concerned with enabling computers to reason, not necessarily by imitating natural intelligence, but rather in their own way. Maria Paola's primary area is automated reasoning, where a reasoning tool is expected to produce solutions also without frequent user interaction, and logico-deductive reasoning, where logic is the representation language and deduction is the main computational mechanism. Automated reasoning has numerous applications, including the analysis, verification, and synthesis of hardware and software systems, planning, natural language understanding, computer mathematics, and education in computer science and mathematics. Automated reasoning is connected with several other fields of computer science, such as machine learning, and symbolic computation. Maria Paola's research topics include:
  • Automated theorem proving based on conflict-driven reasoning (SGGS), or ordering-based inference systems (resolution/superposition), or tableaux-based strategies;
  • Decision procedures for satisfiability modulo theories and assignments (SMA) based on conflict-driven reasoning (CDSAT), or speculative inferences, or generic inferences for theorem proving;
  • Interpolation of proofs for invariant generation or refinement abstraction in model checking;
  • Parallelization of automated reasoning by parallel search;
  • Machine-independent evaluation of strategies and strategy analysis for automated theorem proving.
Maria Paola publishes research papers in international journals that cover automated reasoning, symbolic computation, artificial intelligence, and computational logic (e.g., Journal of Automated Reasoning, ACM Transactions on Computational Logic, Journal of Logic and Computation, Journal of Symbolic Computation, Information and Computation). She regularly attends conferences such as the International Conference on Automated Deduction (CADE), the International Joint Conference on Automated Reasoning (IJCAR), and several others mostly under the umbrella of the Federated Logic Conference (FLoC).

Modules

Modules running in the period selected: 45.
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 Foundations of programming and specification languages (2020/2021)   12  eLearning (Teoria)
Master's degree in Computer Science and Engineering Automated reasoning (2019/2020)   6  eLearning
Bachelor's degree in Computer Science Logic [Matricole dispari] (2019/2020)   6  eLearning
PhD in Computer Science Attività didattica dottorato (2019/2020)   50  eLearning
Master's degree in Computer Science and Engineering Automated reasoning (2018/2019)   6  eLearning
Bachelor's degree in Computer Science Logic [Matricole pari] (2018/2019)   6  eLearning
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 (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 (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 (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 (2010/2011)   12    ALGORITMI PER BIOINFORMATICA
Master's degree in Computer Science and Engineering Automated program verification (2010/2011)   6   
Master's degree in Computer Science and Engineering Algorithms (2009/2010)   12    INTELLIGENZA ARTIFICIALE
Bachelor's degree in Bioinformatics Algorithms (2009/2010)   12    ALGORITMI PER BIOINFORMATICA
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     

 

Research groups

ARLette
Research in automated reasoning
Logica
Logica in matematica ed informatica.
Research interests
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 Machine Intelligence
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 Theory of computation
Logic
Projects
Title Starting date
SGGS Theorem Proving: Algorithms and Implementation 3/23/17
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




Organization

Department facilities