activity
20162022
most citedFormal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version)

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

collaborators

13 papers

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

Petri Nets with Parameterised Data: Modelling and Verification (Extended Version)

Silvio Ghilardi, Alessandro Gianola, Marco Montali +1

During the last decade, various approaches have been put forward to integrate business processes with different types of data. Each of such approaches reflects specific demands in…

math.LO2020

Diego's Theorem for nuclear implicative semilattices

Guram Bezhanishvili, Nick Bezhanishvili, Luca Carai +3

We prove that the variety of nuclear implicative semilattices is locally finite, thus generalizing Diego's Theorem. The key ingredients of our proof include the coloring technique…

cs.LO2019

Combined Covers and Beth Definability (Extended Version)

Diego Calvanese, Silvio Ghilardi, Alessandro Gianola +2

In ESOP 2008, Gulwani and Musuvathi introduced a notion of cover and exploited it to handle infinite-state model checking problems. Motivated by applications to the verification of…

cs.LO20193 cited

Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version)

Diego Calvanese, Silvio Ghilardi, Alessandro Gianola +2

We propose DAB -- a data-aware extension of BPMN where the process operates over case and persistent data (partitioned into a read-only database called catalog and a read-write dat…

cs.LO20192 cited

Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN

Diego Calvanese, Silvio Ghilardi, Alessandro Gianola +2

We propose DAB -- a data-aware extension of the BPMN de-facto standard with the ability of operating over case and persistent data (partitioned into a read-only catalog and a read-…