73 citations · 149 across the 21 of their papers we have counts for
25 papers
Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)
Silvio Ghilardi, Alessandro Gianola, Marco Montali +1
Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management, and Dat…
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…
Admissibility of -Inference Rules: interpolation, model completion, and contact algebras
Nick Bezhanishvili, Luca Carai, Silvio Ghilardi +1
We devise three strategies for recognizing admissibility of non-standard inference rules via interpolation, uniform interpolation, and model completions. We apply our machinery to…
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…
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…
Uniform Interpolants in EUF: Algorithms using DAG-representations
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
The concept of uniform interpolant for a quantifier-free formula from a given formula with a list of symbols, while well-known in the logic literature, has been unknown to the form…
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…
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…
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…
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-…
Free Heyting Algebra Endomorphisms: Ruitenburg's Theorem and Beyond
Silvio Ghilardi, Luigi Santocanale
Ruitenburg's Theorem says that every endomorphism f of a finitely generated free Heyting algebra is ultimately periodic if f fixes all the generators but one. More precisely, there…
Verification of Data-Aware Processes via Array-Based Systems (Extended Version)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola +2
We study verification over a general model of artifact-centric systems, to assess (parameterized) safety properties irrespectively of the initial database instance. We view such ar…
Quantifier Elimination for Database Driven Verification
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola +2
Running verification tasks in database driven systems requires solving quantifier elimination problems of a new kind. These quantifier elimination problems are related to the notio…
Ruitenburg's Theorem via Duality and Bounded Bisimulations
Luigi Santocanale, Silvio Ghilardi
For a given intuitionistic propositional formula A and a propositional variable x occurring in it, define the infinite sequence of formulae { A \_i | i1} by letting A\_1 be A…
Fixed-point elimination in the Intuitionistic Propositional Calculus (extended version)
Silvio Ghilardi, Maria Joao Gouveia, Luigi Santocanale
It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras-that is, the alge- braic models of the Intuitionistic Pr…
Counter Simulations via Higher Order Quantifier Elimination: a preliminary report
Silvio Ghilardi, Elena Pagani
Quite often, verification tasks for distributed systems are accomplished via counter abstractions. Such abstractions can sometimes be justified via simulations and bisimulations. I…
Existentially Closed Brouwerian Semilattices
Luca Carai, Silvio Ghilardi
The variety of Brouwerian semilattices is amalgamable and locally finite, hence by well-known results due to W. H. Wheeler, it has a model completion (whose models are the existent…
Monadic second order logic as the model companion of temporal logic
Silvio Ghilardi, Samuel J. van Gool
The main focus of this paper is on bisimulation-invariant MSO, and more particularly on giving a novel model-theoretic approach to it. In model theory, a model companion of a theor…
Counting Constraints in Flat Array Fragments
Francesco Alberti, Silvio Ghilardi, Elena Pagani
We identify a fragment of Presburger arithmetic enriched with free function symbols and cardinality constraints for interpreted sets, which is amenable to automated analysis. We es…
Fixed-point elimination in the intuitionistic propositional calculus
Silvio Ghilardi, Maria Joao Gouveia, Luigi Santocanale
It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras-that is, the algebraic models of the Intuitionistic Prop…
A model-theoretic characterization of monadic second order logic on infinite words
Silvio Ghilardi, Samuel J. van Gool
Monadic second order logic and linear temporal logic are two logical formalisms that can be used to describe classes of infinite words, i.e., first-order models based on the natura…
Monotonic Abstraction Techniques: from Parametric to Software Model Checking
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Monotonic abstraction is a technique introduced in model checking parameterized distributed systems in order to cope with transitions containing global conditions within guards. Th…
Quantifier-Free Interpolation of a Theory of Arrays
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on t…
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories…