Maria Paola Bonacina

Curriculum

•   Curriculum vitae - EN   (pdf, en, 267 KB, 10/06/21)
•   Curriculum vitae - IT   (pdf, it, 267 KB, 10/06/21)

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).

 

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

---

Maria Paola Bonacina

Office	Collegial Body
member	Collegio Didattico di Informatica - Department Computer Science
member	Computer Science Department Council - Department Computer Science