Cospan/Span(Graph): an Algebra for Open, Reconfigurable Automata Networks. - Alessandro Gianola; Stefano Kasangian; Nicoletta Sabadini (CALCO, 2017)

Interpolation, Amalgamation and Combination (The Non-disjoint Signatures Case). - Silvio Ghilardi; Alessandro Gianola (FroCoS, 2017)

Modularity results for interpolation, amalgamation and superamalgamation. - Silvio Ghilardi; Alessandro Gianola (Ann. Pure Appl. Log., 2018)

Quantifier Elimination for Database Driven Verification. - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (CoRR, 2018)

Verification of Data-Aware Processes via Array-Based Systems (Extended Version). - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (CoRR, 2018)

From Model Completeness to Verification of Data Aware Processes. - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (Description Logic, Theory Combination, and All That, 2019)

Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN. - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (BPM, 2019)

Model Completeness, Covers and Superposition. - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (CADE, 2019)

Model Completeness, Covers and Superposition (Abridged Version). - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (CILC, 2019)

Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN. - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (CoRR, 2019)

Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version). - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (CoRR, 2019)

Petri Nets with Parameterised Data - Modelling and Verification. - Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (BPM, 2020)

Combined Covers and Beth Definability. - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (IJCAR (1), 2020)

Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (CILC, 2020)

Compositional Modeling of Biological Systems in CospanSpan(Graph). - Alessandro Gianola; Stefano Kasangian; Desiree Manicardi; Nicoletta Sabadini; Simone Tini (ICTCS, 2020)

A SMT-based Implementation for Safety Checking of Parameterized Multi-Agent Systems. - Paolo Felli; Alessandro Gianola; Marco Montali (PRIMA, 2020)

Compactly Representing Uniform Interpolants for EUF using (conditional) DAGS. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (CoRR, 2020)

Petri Nets with Parameterised Data: Modelling and Verification (Extended Version). - Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (CoRR, 2020)

SMT-based Safety Verification of Parameterised Multi-Agent Systems. - Paolo Felli; Alessandro Gianola; Marco Montali (CoRR, 2020)

Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version). - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (CoRR, 2020)

CospanSpan(Graph): a Compositional Description of the Heart System. - Alessandro Gianola; Stefano Kasangian; Desiree Manicardi; Nicoletta Sabadini; Filippo Schiavio; Simone Tini (Fundam. Informaticae, 2020)

SMT-based verification of data-aware processes: a model-theoretic approach. - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (Math. Struct. Comput. Sci., 2020)

SMT-based Safety Checking of Parameterized Multi-Agent Systems. - Paolo Felli; Alessandro Gianola; Marco Montali (AAAI, 2021)

Exploring the Conformance Space (Extended abstract). - Andrea Burattin; Alessandro Gianola; Hugo A. López 001; Marco Montali (ITBPM@BPM, 2021)

CoCoMoT: Conformance Checking of Multi-perspective Processes via SMT. - Paolo Felli; Alessandro Gianola; Marco Montali; Andrey Rivkin; Sarah Winkler (BPM, 2021)

Delta-BPMN: A Concrete Language and Verifier for Data-Aware BPMN. - Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (BPM, 2021)

SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Preliminary Results). - Diego Calvanese; Alessandro Gianola; Andrea Mazzullo; Marco Montali (Description Logics, 2021)

A Canonical Algebra of Open Transition Systems. - Elena Di Lavore; Alessandro Gianola; Mario Román; Nicoletta Sabadini; Pawel Sobocinski 001 (FACS, 2021)

Interpolation and Amalgamation for Arrays with MaxDiff. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (FoSSaCS, 2021)

Automated Reasoning for Reinforcement Learning Agents in Structured Environments. - Alessandro Gianola; Marco Montali; Matteo Papini (OVERLAY@GandALF, 2021)

AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDiff. - José Abel Castellanos Joo; Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (SMT, 2021)

CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version). - Paolo Felli; Alessandro Gianola; Marco Montali; Andrey Rivkin; Sarah Winkler (CoRR, 2021)

SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version). - Diego Calvanese; Alessandro Gianola; Andrea Mazzullo; Marco Montali (CoRR, 2021)

Model Completeness, Uniform Interpolants and Superposition Calculus. - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (J. Autom. Reason., 2021)

A Modular SMT-based Approach for Data-aware Conformance Checking. - Paolo Felli; Alessandro Gianola; Marco Montali; Andrey Rivkin; Sarah Winkler (OVERLAY@AI*IA, 2022)

Uniform Interpolation for the Automated Verification of Data-Aware Business Processes. - Alessandro Gianola (OVERLAY@AI*IA, 2022)

LTL Modulo Theories over Finite Traces: modeling, verification, open questions. - Alessandro Gianola; Nicola Gigante (OVERLAY@AI*IA, 2022)

Conformance Checking with Uncertainty via SMT. - Paolo Felli; Alessandro Gianola; Marco Montali; Andrey Rivkin; Sarah Winkler (BPM, 2022)

SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications. - Alessandro Gianola (BPM (PhD/Demos), 2022)

Linear Temporal Logic Modulo Theories over Finite Traces. - Luca Geatti; Alessandro Gianola; Nicola Gigante (IJCAI, 2022)

General Interpolation and Strong Amalgamation for Contiguous Arrays. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur; Chiara Naso (CoRR, 2022)

Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version). - Luca Geatti; Alessandro Gianola; Nicola Gigante (CoRR, 2022)

Conformance Checking with Uncertainty via SMT (Extended Version). - Paolo Felli; Alessandro Gianola; Marco Montali; Andrey Rivkin; Sarah Winkler (CoRR, 2022)

Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version). - Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (CoRR, 2022)

Petri net-based object-centric processes with read-only data. - Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (Inf. Syst., 2022)

Combination of Uniform Interpolants via Beth Definability. - Diego Calvanese; Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (J. Autom. Reason., 2022)

Uniform Interpolants in EUF: Algorithms using DAG-representations. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (Log. Methods Comput. Sci., 2022)

SMT Safety Verification of Ontology-Based Processes. - Diego Calvanese; Alessandro Gianola; Andrea Mazzullo; Marco Montali (AAAI, 2023)

The Droid You're Looking For: C-4PM, a Conversational Agent for Declarative Process Mining. - Yago Fontenla-Seco; Sarah Winkler; Alessandro Gianola; Marco Montali; Manuel Lama Penín; Alberto José Bugarín Diz (BPM (Demos / Resources Forum), 2023)

Approximating Multi-perspective Trace Alignment Using Trace Encodings. - Alessandro Gianola; Jonghyeon Ko; Fabrizio Maria Maggi; Marco Montali; Sarah Winkler (BPM, 2023)

Decidable Fragments of LTLf Modulo Theories. - Luca Geatti; Alessandro Gianola; Nicola Gigante; Sarah Winkler (ECAI, 2023)

Safety Verification and Universal Invariants for Relational Action Bases. - Silvio Ghilardi; Alessandro Gianola; Marco Montali; Andrey Rivkin (IJCAI, 2023)

Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories (Extended Abstract). - Luca Geatti; Alessandro Gianola; Nicola Gigante (TIME, 2023)

Decidable Fragments of LTLf Modulo Theories (Extended Version). - Luca Geatti; Alessandro Gianola; Nicola Gigante; Sarah Winkler (CoRR, 2023)

Linear-Time Verification of Data-Aware Processes Modulo Theories via Covers and Automata (Extended Version). - Alessandro Gianola; Marco Montali; Sarah Winkler (CoRR, 2023)

Object-Centric Conformance Alignments with Synchronization (Extended Version). - Alessandro Gianola; Marco Montali; Sarah Winkler (CoRR, 2023)

Verification of Data-Aware Processes via Satisfiability Modulo Theories - Alessandro Gianola (Springer, 2023)

Span(Graph): a canonical feedback algebra of open transition systems. - Elena Di Lavore; Alessandro Gianola; Mario Román; Nicoletta Sabadini; Pawel Sobocinski 001 (Softw. Syst. Model., 2023)

Data-aware conformance checking with SMT. - Paolo Felli; Alessandro Gianola; Marco Montali; Andrey Rivkin; Sarah Winkler (Inf. Syst., 2023)

Interpolation Results for Arrays with Length and MaxDiff. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur; Chiara Naso (ACM Trans. Comput. Log., 2023)

Multi-perspective conformance checking of uncertain process traces: An SMT-based approach. - Paolo Felli; Alessandro Gianola; Marco Montali; Andrey Rivkin; Sarah Winkler (Eng. Appl. Artif. Intell., 2023)

Linear-Time Verification of Data-Aware Processes Modulo Theories via Covers and Automata. - Alessandro Gianola; Marco Montali; Sarah Winkler (AAAI, 2024)

Glocal Conformance Checking. - Alessandro Burigana; Alessandro Gianola; Marco Montali; Sarah Winkler (BPM, 2024)

Object-Centric Conformance Alignments with Synchronization. - Alessandro Gianola; Marco Montali; Sarah Winkler (CAiSE, 2024)

A General Automata Model for First-Order Temporal Logics (Extended Version). - Luca Geatti; Alessandro Gianola; Nicola Gigante (CoRR, 2024)

First-Order Automata. - Luca Geatti; Alessandro Gianola; Nicola Gigante (AAAI, 2025)

Efficient Conformance Checking of Rich Data-Aware Declare Specifications. - Jacobo Casas-Ramos; Sarah Winkler; Alessandro Gianola; Marco Montali; Manuel Mucientes; Manuel Lama (BPM, 2025)

Constraint-Based Reasoning and Analysis for BPM: CSP to the Rescue. - Alessandro Gianola; Andrey Rivkin; Mateusz Slazynski (BPM, 2025)

Object-Centric Processes with Structured Data and Exact Synchronization - Formal Modelling and Conformance Checking. - Alessandro Gianola; Marco Montali; Sarah Winkler (CAiSE (2), 2025)

Approximate conformance checking: Fast computation of multi-perspective, probabilistic alignments. - Alessandro Gianola; Jonghyeon Ko; Fabrizio Maria Maggi; Marco Montali; Sarah Winkler (Inf. Syst., 2025)

Object-centric Processes with Structured Data and Exact Synchronization (Extended Version). - Alessandro Gianola; Marco Montali; Sarah Winkler (CoRR, 2025)

Efficient Conformance Checking of Rich Data-Aware Declare Specifications (Extended). - Jacobo Casas-Ramos; Sarah Winkler; Alessandro Gianola; Marco Montali; Manuel Mucientes; Manuel Lama (CoRR, 2025)