Skip to content
Publications
Journal Papers
- S. Ghilardi and A. Gianola, Modularity Results for Interpolation, Amalgamation and Superamalgamation. Annals of Pure and Applied Logic, volume 169, issue 8, 2018. (Link)
- 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)
- 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)
- 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)
- 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)
- 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)
- 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)
- 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)
- 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)
- P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler. Data-aware Conformance Checking with SMT. Information Systems, 2023. (Link)
- 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
- S. Ghilardi and A. Gianola, Interpolation, Amalgamation and Combination (the non-disjoint signatures case). Proceedings of FroCoS 2017, LNAI, Springer, 2017. (Link)
- 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)
- D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Model Completeness, Covers and Superposition. Proceedings of CADE-27, LNAI, Springer, 2019. (Link)
- 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)
- D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Combined Covers and Beth Definability. Proceedings of IJCAR 2020, LNAI, Springer, 2020. (Link)
- 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)
- 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)
- 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)
- 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)
- P. Felli, A. Gianola, M. Montali. SMT-based Safety Checking of Parameterized Multi-Agent Systems. Proceedings of AAAI 2021. AAAI Press. 2021. (Link)
- S. Ghilardi, A. Gianola, D. Kapur. Interpolation and Amalgamation for Arrays with MaxDiff. Proceedings of FoSSaCS 2021, LNCS, Springer. 2021. (Link)
- 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)
- 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)
- 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)
- L. Geatti, A. Gianola, N. Gigante. Linear Temporal Logic Modulo Theories over Finite Traces. Proceedings of IJCAI 2022. 2022. (Link)
- P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler. Conformance Checking with Uncertainty via SMT. Proceedings of BPM 2022, LNCS. Springer. 2022. (Link)
- 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)
- D. Calvanese, A. Gianola, A. Mazzullo, M. Montali. SMT Safety Verification of Ontology-Based Processes. Proceedings of AAAI 2023. 2023. (Link)
- S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. Safety Verification and Universal Invariants for Relational Action Bases. Proceedings of IJCAI 2023. 2023. (Link)
- 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)
- 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)
Book Chapters
- 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)
Workshop Papers with Refereed Proceedings
- 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)
- 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)
- 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)
- 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)
- 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)
- 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)
- 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)
- 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
Preprints
- D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Verification of Data-Aware Processes via Array-Based Systems (Extended Version). Technical Report arXiv:1806.11459, arXiv.org, 2018.
- D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Quantifier Elimination for Database Driven Verification. Technical Report arXiv:1806.09686, arXiv.org, 2018.
- D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Formal Modeling and SMT-based Parameterized Verification of Data-Aware BPMN (Extended Version). Technical Report arXiv:1906.07811, arXiv.org, 2019.
- D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Formal Modeling and SMT-based Parameterized Verification of Multi-Case Data-Aware BPMN. Technical Report arXiv:1905.12991, arXiv.org, 2019.
- D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Combined Covers and Beth Definability (Extended Version) . Technical Report arXiv:1911.07774, arXiv.org, 2019.
- S. Ghilardi, A. Gianola, D. Kapur. Compactly Representing Uniform Interpolants for EUF using (conditional) DAGS. Technical Report, 2020. (http://gianola.people.unibz.it/wp-content/uploads/2021/03/Compactly-Representing-UI.pdf)
- A. Gianola, S. Kasangian, D. Manicardi, N. Sabadini, S. Tini. Compositional Modeling of Biological Systems in CospanSpan(Graph) (Extended Version). Technical Report, 2020 (http://gianola.people.unibz.it/wp-content/uploads/2020/07/BioSys-ext.pdf)
- P. Felli, A. Gianola, M. Montali. SMT-based Safety Verification of Parameterised Multi-Agent Systems. Technical Report arXiv:2008.04774, arXiv.org, 2020.
- S. Ghilardi, A. Gianola, D. Kapur. Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version). Technical Report arXiv:2010.07082, arXiv.org, 2020.
- E. Di Lavore, A. Gianola, M. Román, N. Sabadini, P. Sobociński. A canonical algebra of open transition systems. Technical Report arXiv:2010.10069, arXiv.org, 2020.
- P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler. CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version). Technical Report arXiv:2103.10507, arXiv.org, 2021.
- S. Ghilardi, A. Gianola, D. Kapur, C. Naso. General Interpolation and Strong Amalgamation for Contiguous Arrays. Technical Report arXiv:2204.11771, arXiv.org, 2022.
- L. Geatti, A. Gianola, N. Gigante. Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version). Technical Report arXiv:2204.13693, arXiv.org, 2022.
- P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler. Conformance Checking with Uncertainty via SMT (Extended Version). Technical Report arXiv:2206.07461, arXiv.org, 2022.
- S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version). Technical Report arXiv:2208.06377, arXiv.org, 2022.