alessandro.gianola at tecnico.ulisboa.pt

alessandro.gianola at inesc-id.pt

Research

My scientific interests mainly involve formal methods and Business Process Management (BPM): specifically, my research activity focuses on process mining and on theoretical and methodological aspects of logic and formal methods for the verification of complex (business) processes with data.

Awards

• 2023 CADE Bill McCune PhD Award in Automated Reasoning: I was the winner of the 2023 CADE Bill McCune PhD Award in Automated Reasoning, given by CADE Inc. for substantive contributions to the field of Automated Reasoning (https://cadeinc.org/McCune-Award).
• 2022 Best BPM Dissertation award: I was the winner of the 2022 Best BPM Dissertation award, given by the BPM Association at the 20^th International Conference on Business Process Management (BPM 2022).
• 2022 Best Italian PhD Thesis in Theoretical Computer Science award: I was recipient of the 2022 Best Italian PhD Thesis in Theoretical Computer Science award, given by the Italian Chapter of the European Association for Theoretical Computer Science (EATCS), presented at ICTCS 2022.
• Best Paper Award at the 19th International Conference on Business Process Management (BPM 2021), for the paper titled ‘CoCoMoT: Conformance Checking of Multi-perspective Processes via SMT’, co-authored with Paolo Felli, Marco Montali, Andrey Rivkin and Sarah Winkler. (link to the paper).
• Best Paper Award at the 23nd International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2020), for the paper titled ‘A SMT-based Implementation for Safety Checking of Parameterized Multi-Agent Systems’, co-authored with Paolo Felli and Marco Montali. (link to the paper).
• 2019 Woody Bledsoe Award: I was one of the recipients of the 2019 Woody Bledsoe Award given at the 27^th International Conference on Automated Deduction (CADE-27), which is a travel grant that supports students who obtained outstanding achievements in automated reasoning.

Research Groups

• Since September 2023, I have been a member of the Automated Reasoning and Software Reliability (ARSR)  research group at INESC-ID (Lisbon, Portugal), which mission is to enable and support the construction of reliable and dependable software systems with a focus on producing machine-assisted methods to improve the quality and dependability of computer systems.
• Since 2022, I have been a member of the OVERLAY research group on Formal Methods for AI, which fosters collaboration among a diverse team of Formal Methods and AI researchers, aiming at pursuing multidisciplinary research at the border of the two fields.
• From November 2017 to September 2023, I was a member of the KRDB Research Centre for Knowledge and Data at the Faculty of Computer Science of the Free University of Bozen-Bolzano, Italy.

Talks

Invited Talks

• Invited Talk at iPRA 2022, a FLoC 2022 workshop, Haifa, Israel. August 2022.

Presentations of Accepted Papers at International Conferences and Workshops

• 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023), Macao, SAR. August 2023.
• 4th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis (OVERLAY 2022), Udine, Italy. November 2021.
• 10th International Conference on Topology, Algebra and Categories in Logic (TACL 2022), Coimbra, Portugal. June 2022.
• 3rd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis (OVERLAY 2021), Padova, Italy. September 2021.
• 24th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2021), Online. March 2021.
• 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Online. July 2020.
• 35th Italian Conference on Computational Logic (CILC 2020), Rende, Italy. October 2020.
• 27th International Conference on Automated Deduction (CADE 27), Natal, Brazil. August 2019.
• 2nd International ARCADE (Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements) Workshop, Natal, Brazil. August 2019.
• 34th Italian Conference on Computational Logic (CILC 2019), Trieste, Italy. June 2019.
• 33rd Italian Conference on Computational Logic (CILC 2018), Bolzano, Italy. September 2018.

Chair of International Conferences and Workshops

• Co-chair of the 2nd International Workshop on Formal Methods for Business Process Management (FM-BPM 2024), co-located with BPM 2024.
• Co-chair of the 1st International Workshop on Formal Methods for Business Process Management (FM-BPM 2023), co-located with BPM 2023.
• Co-chair of the 5th Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis OVERLAY (part of AIxIA 2023).

Program Committees

• Member of the Program Committee of the 22nd International Conference on Business Process Management (BPM 2024).
• Member of the Program Committee of the 27th European Conference on Artificial Intelligence (ECAI 2024).
• Member of the Program Committee of the 33rd International Joint Conference on Artificial Intelligence (IJCAI 2024).
• Member of the Program Committee of the 38th Annual AAAI Conference on Artificial Intelligence (AAAI 2024).
• Member of the Program Committee of the 22nd International Conference on Business Process Management (BPM 2024).
• Member of the Program Committee of the 26th European Conference on Artificial Intelligence (ECAI 2023).
• Member of the Program Committee of the 21st International Conference on Business Process Management (BPM 2023).
• Member of the Program Committee of the 20th International Conference on Principles of Knowledge Representation and Reasoning (KR 2023).
• Member of the Program Committee of the 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023).
• Member of the Program Committee of the 4th Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis OVERLAY (part of AIxIA 2022).

Organization

• Member of the Local Organization Committee of the 4th International Conference on Process Mining (ICPM 2022), October 23-28, 2022.

Teaching

Publications

Peer-reviewed Journal Papers

1. S. Ghilardi and A. Gianola, Modularity Results for Interpolation, Amalgamation and Superamalgamation. Annals of Pure and Applied Logic, volume 169, issue 8, 2018. (Link)
2. A. Gianola, S. Kasangian, D. Manicardi, N. Sabadini, F. Schiavio, S. Tini. CospanSpan(Graph): a compositional description of the heart system. Fundamenta Informaticae, volume 171 (1-4), 2020.  (Link)
3. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. SMT-based Verification of Data-Aware Processes: a Model-Theoretic Approach. Mathematical Structures in Computer Science, volume 30, issue 3, 2020. (Link)
4. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. Model completeness, Uniform Interpolants and Superposition Calculus. Journal of Automated Reasoning, volume 65, issue 7, 2021. (Link)
5. S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Petri Net-Based Object-Centric Processes with Read-Only Data. Information Systems, volume 107, 2022. (Link)
6. S. Ghilardi, A. Gianola, and D. Kapur. Uniform Interpolants in EUF: Algorithms using DAG-representations. Logical Methods in Computer Science, volume 18, issue 2, 2022. (Link)
7. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. Combination of Uniform Interpolants via Beth Definability. Journal of Automated Reasoning, volume 66, issue 3, 2022. (Link)
8. E. Di Lavore, A. Gianola, M. Román, N. Sabadini, P. Sobociński. Span(Graph): a Canonical Feedback Algebra of Open Transition Systems, Software and Systems Modeling, volume 22, issue 2, 2023. (Link)
9. S. Ghilardi, A. Gianola, D. Kapur, C. Naso. Interpolation Results for Arrays with Length and MaxDiff. ACM Transactions on Computational Logic, volume 24, issue 4, 2023. (Link)
10. P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler. Data-aware Conformance Checking with SMT. Information Systems, 2023. (Link)
11. P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler. Multi-perspective conformance checking of uncertain process traces: An SMT-based approach. Engineering Applications of Artificial Intelligence, 2023. (Link)

Conference Papers with Refereed Proceedings

12. S. Ghilardi and A. Gianola, Interpolation, Amalgamation and Combination (the non-disjoint signatures case). Proceedings of FroCoS 2017, LNAI, Springer, 2017. (Link)
13. A. Gianola, S. Kasangian and N. Sabadini. Cospan/Span(Graph): an Algebra for Open, Reconfigurable Automata Networks. Proceedings of CALCO 2017, Schloss Dagstuhl: LIPIcs, 2017. (Link)
14. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Model Completeness, Covers and Superposition. Proceedings of CADE-27, LNAI, Springer, 2019. (Link)
15. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Formal Modeling and SMT-based Parameterized Verification of Data-Aware BPMN. Proceedings of BPM 2019, LNCS, Springer, 2019. (Link)
16. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Combined Covers and Beth Definability. Proceedings of IJCAR 2020, LNAI, Springer, 2020. (Link)
17. S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Petri Nets with Parameterised Data: Modelling and Verification. Proceedings of BPM 2020, LNCS, Springer, 2020. (Link)
18. A. Gianola, S. Kasangian, D. Manicardi, N. Sabadini, S. Tini. Compositional Modeling of Biological Systems in CospanSpan(Graph). Proceedings of ICTCS 2020,  CEUR-WS, 2020. (Link)
19. S. Ghilardi, A. Gianola, D. Kapur, Computing Uniform Interpolants for EUF via  (conditional) DAG-based Compact Representations. Proceedings of CILC 2020, CEUR-WS, 2020. (Link)
20. P. Felli, A. Gianola, M. Montali. A SMT-based Implementation for Safety Checking of Parameterized Multi-Agent Systems. Proceedings of PRIMA 2020, LNCS, Springer, 2021. Best Paper Award. (Link)
21. P. Felli, A. Gianola, M. Montali. SMT-based Safety Checking of Parameterized Multi-Agent Systems. Proceedings of AAAI 2021. AAAI Press. 2021. (Link)
22. S. Ghilardi, A. Gianola, D. Kapur. Interpolation and Amalgamation for Arrays with MaxDiff. Proceedings of FoSSaCS 2021, LNCS, Springer. 2021. (Link)
23. P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler. CoCoMoT: Conformance Checking of Multi-perspective Processes via SMT. Proceedings of BPM 2021, LNCS. Springer. 2021. Best Paper Award. (Link)
24. S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. Delta-BPMN: a Concrete Language and Verifier for Data-aware BPMN. Proceedings of BPM 2021, LNCS. Springer. 2021. (Link)
25. E. Di Lavore, A. Gianola, M. Román, N. Sabadini, P. Sobociński. A canonical algebra of open transition systems. Proceedings of FACS 2021, LNCS. Springer. 2021. (Link)
26. L. Geatti, A. Gianola, N. Gigante. Linear Temporal Logic Modulo Theories over Finite Traces. Proceedings of IJCAI 2022. 2022. (Link)
27. P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler. Conformance Checking with Uncertainty via SMT. Proceedings of BPM 2022, LNCS. Springer. 2022. (Link)
28. A. Gianola. SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications (Extended Abstract). Proceedings of BPM (PhD/Demos). CEUR-Worksop Proceedings. 2022. (Link)
29. D. Calvanese, A. Gianola, A. Mazzullo, M. Montali. SMT Safety Verification of Ontology-Based Processes. Proceedings of AAAI 2023. 2023. (Link)
30. S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. Safety Verification and Universal Invariants for Relational Action Bases. Proceedings of IJCAI 2023. 2023. (Link)
31. A. Gianola, J. Ko, F. M. Maggi, M. Montali, S. Winkler. Approximating Multi-Perspective Trace Alignment Using Trace Encoding. Proceeding of BPM 2023. 2023. (Link)
32. Y. Fontenla-Seco, S. Winkler, A. Gianola, M. Montali, M. Lama and A. Bugarín-Diz. The Droid You’re Looking For: C-4PM, a Conversational Agent for Declarative Process Mining. Proceeding of BPM 2023 (Demo). 2023 (Link)
33. L. Geatti, A. Gianola, N. Gigante, S. Winkler. Decidable Fragments of LTLf Modulo Theories. Proceedings of ECAI 2023. 2023 (Link)
34. A. Gianola, M. Montali, S. Winkler. Linear-Time Verification of Data-Aware Processes Modulo Theories via Covers and Automata. Proceedings of AAAI 2024. Accepted. To appear.

Book Chapters

35. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. From Model Completeness to Verification of Data Aware Processes. In C. Lutz, U. Sattler, C. Tinelli, A.-Y. Turhan, and F. Wolter, editors, Description Logic, Theory Combination, and All That, pages 212–239, Springer, 2019. (Link)

Authored Books

36. A. Gianola. Verification of Data Aware Processes via Satisfiability Modulo Theories. LNBIP, volume 470. Springer, 2023. (Link)

Workshop Papers with Refereed Proceedings

37. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Verification of Data-Aware Processes: Challenges and Opportunities for Automated Reasoning. Proceedings of ARCADE 2019, 2nd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements. EPTCS, volume 311, pp. 53–58. 2019. (Link)
38. J. A. Castellanos Joo, S. Ghilardi, A. Gianola and D. Kapur. AXDInterpolator: a Tool for Computing Interpolants for Arrays with MaxDiff. Proceedings of SMT 2021. CEUR-WS, volume 2908, pp. 40-52. 2021 (Link)
39. A. Burattin, A. Gianola, H. A. López and M. Montali. Exploring the Conformance Space (Extended Abstract). Proceedings of ITBPM 2021, CEUR-WS, volume 2952, pp. 62-67. 2021 (Link)
40. D. Calvanese, A. Gianola, A. Mazzullo and M. Montali. SMT-Based Verification of Data-Aware Processes under Ontologies (Preliminary Results). Proceedings of DL 2021. CEUR-WS, volume 2954, pp. 1-15. 2021 (Link)
41. A. Gianola, M. Montali, M. Papini. Automated Reasoning for Reinforcement Learning Agents in Structured Environments. Proceedings of OVERLAY 2021. CEUR-WS, volume 2987, pp. 43-48. 2021 (Link)
42. A. Gianola. Uniform Interpolation for the Automated Verification of Data-Aware Business Processes. Proceedings of OVERLAY 2022. CEUR-WS, volume 3311, pp. 73-79. 2022 (Link)
43. A. Gianola, N. Gigante. LTL Modulo Theories over Finite Traces: modeling, verification, open questions. Proceedings of OVERLAY 2022. CEUR-WS, volume 3311, pp. 13-19. 2022 (Link)
44. P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler. A Modular SMT-based Approach for Data-aware Conformance Checking. Proceedings of OVERLAY 2022. CEUR-WS, volume 3311, pp. 87-92. 2022 (Link)

PhD Dissertation

• A. Gianola, SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications. PhD Dissertation, Free University of Bozen-Bolzano, Bolzano, Italy. 2022, BIA: Bozen-Bolzano Institutional Archive. (Link)