activity
20182022
most citedLinear Temporal Logic Modulo Theories over Finite Traces (Extended Version)

3 citations · 12 across the 8 of their papers we have counts for

collaborators

12 papers

cs.LO20223 cited

Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)

Luca Geatti, Alessandro Gianola, Nicola Gigante

This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spir…

cs.LO2022

General Interpolation and Strong Amalgamation for Contiguous Arrays

Silvio Ghilardi, Alessandro Gianola, Deepak Kapur +1

Interpolation is an essential tool in software verification, where first-order theories are used to constrain datatypes manipulated by programs. In this paper, we introduce the dat…

cs.AI20211 cited

SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version)

Diego Calvanese, Alessandro Gianola, Andrea Mazzullo +1

In the context of verification of data-aware processes (DAPs), a formal approach based on satisfiability modulo theories (SMT) has been considered to verify parameterised safety pr…

cs.AI20212 cited

CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version)

Paolo Felli, Alessandro Gianola, Marco Montali +2

Conformance checking is a key process mining task for comparing the expected behavior captured in a process model and the actual behavior recorded in a log. While this problem has…

cs.LO2020

Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version)

Silvio Ghilardi, Alessandro Gianola, Deepak Kapur

In this paper, the theory of McCarthy's extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. I…

cs.AI20201 cited

SMT-based Safety Verification of Parameterised Multi-Agent Systems

Paolo Felli, Alessandro Gianola, Marco Montali

In this paper we study the verification of parameterised multi-agent systems (MASs), and in particular the task of verifying whether unwanted states, characterised as a given state…