Publications

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, accepted. To appear.
  9. S. Ghilardi, A. Gianola, D. Kapur, C. Naso. Interpolation Results for Arrays with Length and MaxDiff. ACM Transactions on Computational Logic, accepted. To appear.

Conference Papers with Refereed Proceedings

  1. S. Ghilardi and A. Gianola, Interpolation, Amalgamation and Combination (the non-disjoint signatures case). Proceedings of FroCoS 2017, LNAI, Springer, 2017. (Link)
  2. 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)
  3. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Model Completeness, Covers and Superposition. Proceedings of CADE-27, LNAI, Springer, 2019. (Link)
  4. 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)
  5. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Combined Covers and Beth Definability. Proceedings of IJCAR 2020, LNAI, Springer, 2020. (Link)
  6. 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)
  7. 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)
  8. 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)
  9. 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)
  10. P. Felli, A. Gianola, M. Montali. SMT-based Safety Checking of Parameterized Multi-Agent Systems. Proceedings of AAAI 2021. AAAI Press. 2021. (Link)
  11. S. Ghilardi, A. Gianola, D. Kapur. Interpolation and Amalgamation for Arrays with MaxDiff. Proceedings of FoSSaCS 2021, LNCS, Springer. 2021. (Link)
  12. 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)
  13. 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)
  14. 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)
  15. L. Geatti, A. Gianola, N. Gigante. Linear Temporal Logic Modulo Theories over Finite Traces. Proceedings of IJCAI 2022. 2022. (Link)
  16. P. Felli, A. Gianola, M. Montali, A. Rivkin, S. Winkler. Conformance Checking with Uncertainty via SMT. Proceedings of BPM 2022, LNCS. Springer. 2022. (Link)
  17. 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)
  18. D. Calvanese, A. Gianola, A. Mazzullo, M. Montali. SMT Safety Verification of Ontology-Based Processes. Proceedings of AAAI 2023. Accepted. To appear.
  19. S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. Safety Verification and Universal Invariants for Relational Action Bases. Proceedings of IJCAI 2023. Accepted. To appear.

Book Chapters

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

  1. 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)
  2. 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)
  3. 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)
  4. 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)
  5. 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)
  6. 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)
  7. 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)
  8. 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)

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.