Publications

Journal Papers

• S. Ghilardi and A. Gianola, Modularity Results for Interpolation, Amalgamation and Superamalgamation. Annals of Pure and Applied Logic, Volume 169, n. 8, 2018. (https://www.sciencedirect.com/science/article/pii/S016800721830037X)
• 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.  (https://content.iospress.com/articles/fundamenta-informaticae/fi1880)
• 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. (https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/smtbased-verification-of-dataaware-processes-a-modeltheoretic-approach/83C5D41802478A43B47EB4F3BEBF08CC)
• D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. Model completeness, Uniform Interpolants and Superposition Calculus (with Applications to Verification of Data-Aware Processes). Journal of Automated Reasoning. To appear.

Conference Papers

• S. Ghilardi and A. Gianola, Interpolation, Amalgamation and Combination (the non-disjoint signatures case). Proceedings of FroCoS 2017, LNAI, Springer, 2017. (https://link.springer.com/chapter/10.1007/978-3-319-66167-4_18)
• 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. (http://drops.dagstuhl.de/opus/volltexte/2017/8053/)
• D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Model Completeness, Covers and Superposition. Proceedings of CADE-27, LNAI, Springer, 2019. (https://link.springer.com/chapter/10.1007/978-3-030-29436-6_9)
• 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. (https://link.springer.com/chapter/10.1007/978-3-030-26619-6_12)
• D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Combined Covers and Beth Definability. Proceedings of IJCAR 2020, LNAI, Springer, 2020. (https://link.springer.com/chapter/10.1007/978-3-030-51074-9_11)
• S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Petri Nets with Parameterised Data: Modelling and Verification. Proceedings of BPM 2020, LNCS, Springer, 2020. (https://link.springer.com/chapter/10.1007%2F978-3-030-58666-9_4)
• 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. (http://ceur-ws.org/Vol-2756/paper_6.pdf)
• S. Ghilardi, A. Gianola, D. Kapur, Computing Uniform Interpolants for EUF via  (conditional) DAG-based Compact Representations. Proceedings of CILC 2020, CEUR-WS, 2020. (http://ceur-ws.org/Vol-2710/paper5.pdf)
• 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.(https://link.springer.com/chapter/10.1007/978-3-030-69322-0_17)
• P. Felli, A. Gianola, M. Montali. SMT-based Safety Checking of Parameterized Multi-Agent Systems. Proceedings of AAAI 2021. To appear.
• S. Ghilardi, A. Gianola, D. Kapur. Interpolation and Amalgamation for Arrays with MaxDiff. Proceedings of FoSSaCS 2021, LNCS, Springer. 2021 (https://link.springer.com/chapter/10.1007/978-3-030-71995-1_14)

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. (https://link.springer.com/chapter/10.1007/978-3-030-22102-7_10)

Workshop Papers

• 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. (http://eptcs.web.cse.unsw.edu.au/paper.cgi?ARCADE2019.9)

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. (http://gianola.people.unibz.it/wp-content/uploads/2019/07/Verification.pdf)
• 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. (http://gianola.people.unibz.it/wp-content/uploads/2019/07/QE.pdf)
• 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. (http://gianola.people.unibz.it/wp-content/uploads/2019/07/BPM-long.pdf)
• 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. (http://gianola.people.unibz.it/wp-content/uploads/2019/07/BPM-long-techrep.pdf)
• 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. (http://gianola.people.unibz.it/wp-content/uploads/2020/04/CombinedCovers.pdf)
• 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.