Silvio Ghilardi

ORCID

Publication Activity (10 Years)

Years Active: 1989-2024
Publications (10 Years): 59

Top Venues

Publications

Matteo De Berardinis, Silvio Ghilardi
Profiniteness, monadicity and universal models in modal logic. Ann. Pure Appl. Log. 175 (7) (2024)
Silvio Ghilardi, Lia M. Poidomani
Model Completeness for Rational Trees. IJCAR (1) (2024)
Rodrigo Nicolau Almeida, Silvio Ghilardi
-rules. CoRR (2024)
Nick Bezhanishvili, Luca Carai, Silvio Ghilardi, Lucia Landi
-Inference Rules: interpolation, model completion, and contact algebras. Ann. Pure Appl. Log. 174 (1) (2023)
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur, Chiara Naso
Interpolation Results for Arrays with Length and MaxDiff. ACM Trans. Comput. Log. 24 (4) (2023)
Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Safety Verification and Universal Invariants for Relational Action Bases. IJCAI (2023)
Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Petri net-based object-centric processes with read-only data. Inf. Syst. 107 (2022)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Combination of Uniform Interpolants via Beth Definability. J. Autom. Reason. 66 (3) (2022)
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
Uniform Interpolants in EUF: Algorithms using DAG-representations. Log. Methods Comput. Sci. 18 (2) (2022)
Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi, Elena Pagani
A Formal Verification of ArpON - A Tool for Avoiding Man-in-the-Middle Attacks in Ethernet Networks. IEEE Trans. Dependable Secur. Comput. 19 (6) (2022)
Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version). CoRR (2022)
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur, Chiara Naso
General Interpolation and Strong Amalgamation for Contiguous Arrays. CoRR (2022)
Silvio Ghilardi, Elena Pagani
Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems. J. Autom. Reason. 65 (3) (2021)
José Abel Castellanos Joo, Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDiff. SMT (2021)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Model Completeness, Uniform Interpolants and Superposition Calculus. J. Autom. Reason. 65 (7) (2021)
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
Interpolation and Amalgamation for Arrays with MaxDiff. FoSSaCS (2021)
Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Delta-BPMN: A Concrete Language and Verifier for Data-Aware BPMN. BPM (2021)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Combined Covers and Beth Definability. IJCAR (1) (2020)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
SMT-based verification of data-aware processes: a model-theoretic approach. Math. Struct. Comput. Sci. 30 (3) (2020)
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
Compactly Representing Uniform Interpolants for EUF using (conditional) DAGS. CoRR (2020)
Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Petri Nets with Parameterised Data - Modelling and Verification. BPM (2020)
Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Petri Nets with Parameterised Data: Modelling and Verification (Extended Version). CoRR (2020)
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version). CoRR (2020)
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations. CILC (2020)
Silvio Ghilardi, Luigi Santocanale
Free Heyting algebra endomorphisms: Ruitenburg's Theorem and beyond. Math. Struct. Comput. Sci. 30 (6) (2020)
Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale
Fixed-point Elimination in the Intuitionistic Propositional Calculus. ACM Trans. Comput. Log. 21 (1) (2020)
Nick Bezhanishvili, Silvio Ghilardi, Lucia Landi
-rules: The Case of Contact Algebras. AiML (2020)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN. BPM (2019)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Model Completeness, Covers and Superposition. CADE (2019)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Combined Covers and Beth Definability. CoRR (2019)
Luca Carai, Silvio Ghilardi
Existentially closed Brouwerian Semilattices. J. Symb. Log. 84 (4) (2019)
Silvio Ghilardi, Luigi Santocanale
Free Heyting Algebra Endomorphisms: Ruitenburg's Theorem and Beyond. CoRR (2019)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version). CoRR (2019)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN. CoRR (2019)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
From Model Completeness to Verification of Data Aware Processes. Description Logic, Theory Combination, and All That (2019)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Model Completeness, Covers and Superposition (Abridged Version). CILC (2019)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Verification of Data-Aware Processes via Array-Based Systems (Extended Version). CoRR (2018)
Silvio Ghilardi, Luigi Santocanale
Ruitenburg's Theorem via Duality and Bounded Bisimulations. Advances in Modal Logic (2018)
Luigi Santocanale, Silvio Ghilardi
Ruitenburg's Theorem via Duality and Bounded Bisimulations. CoRR (2018)
Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale
Fixed-point elimination in the Intuitionistic Propositional Calculus (extended version). CoRR (2018)
Silvio Ghilardi, Alessandro Gianola
Modularity results for interpolation, amalgamation and superamalgamation. Ann. Pure Appl. Log. 169 (8) (2018)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
Quantifier Elimination for Database Driven Verification. CoRR (2018)
Silvio Ghilardi, Elena Pagani
Counter Simulations via Higher Order Quantifier Elimination: a preliminary report. PxTP (2017)
Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi, Elena Pagani
Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study -. IFM (2017)
Nick Bezhanishvili, Silvio Ghilardi, Frederik Möllerström Lauridsen
One-step Heyting Algebras and Hypersequent Calculi with the Bounded Proof Property. J. Log. Comput. 27 (7) (2017)
Silvio Ghilardi, Samuel J. van Gool
A Model-Theoretic characterization of Monadic second order Logic on Infinite Words. J. Symb. Log. 82 (1) (2017)
Silvio Ghilardi, Elena Pagani
Second Order Quantifier Elimination: Towards Verification Applications. SOQE (2017)
Silvio Ghilardi, Alessandro Gianola
Interpolation, Amalgamation and Combination (The Non-disjoint Signatures Case). FroCoS (2017)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
A Framework for the Verification of Parameterized Infinite-state Systems. Fundam. Informaticae 150 (1) (2017)
Marcello M. Bersani, Francesco Marconi, Matteo Rossi, Madalina Erascu, Silvio Ghilardi
Formal verification of data-intensive applications through model checking modulo theories. SPIN (2017)
Francesco Alberti, Silvio Ghilardi, Elena Pagani
Cardinality constraints for arrays (decidability results and applications). Formal Methods Syst. Des. 51 (3) (2017)
Nick Bezhanishvili, David Gabelaia, Silvio Ghilardi, Mamuka Jibladze
Admissible Bases Via Stable Canonical Rules. Stud Logica 104 (2) (2016)
Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale
Fixed-point elimination in the intuitionistic propositional calculus. CoRR (2016)
Silvio Ghilardi, Samuel J. van Gool
Monadic second order logic as the model companion of temporal logic. CoRR (2016)
Francesco Alberti, Silvio Ghilardi, Elena Pagani
Counting Constraints in Flat Array Fragments. CoRR (2016)
Francesco Alberti, Silvio Ghilardi, Elena Pagani
Counting Constraints in Flat Array Fragments. IJCAR (2016)
Francesco Alberti, Silvio Ghilardi, Andrea Orsini, Elena Pagani
Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies. CILC (2016)
Silvio Ghilardi, Sam van Gool
Monadic second order logic as the model companion of temporal logic. LICS (2016)
Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale
Fixed-Point Elimination in the Intuitionistic Propositional Calculus. FoSSaCS (2016)
Silvio Ghilardi, Samuel J. van Gool
A model-theoretic characterization of monadic second order logic on infinite words. CoRR (2015)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Decision Procedures for Flat Array Properties. J. Autom. Reason. 54 (4) (2015)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
A New Acceleration-Based Combination Framework for Array Properties. FroCos (2015)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15 (1) (2014)
Nick Bezhanishvili, Silvio Ghilardi
The bounded proof property via step algebras and step frames. Ann. Pure Appl. Log. 165 (12) (2014)
Nick Bezhanishvili, Silvio Ghilardi
Multiple-conclusion Rules, Hypersequents Syntax and Step Frames. Advances in Modal Logic (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
A Framework for the Verification of Parameterized Infinite-State Systems. CILC (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Monotonic Abstraction Techniques: from Parametric to Software Model Checking. MOD* (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Decision Procedures for Flat Array Properties. TACAS (2014)
Silvio Ghilardi, Grigori Mints
The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination. Log. J. IGPL 22 (4) (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Decision Procedures for Flat Array Properties. SMT (2014)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45 (1) (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Booster: An Acceleration-Based Verification Framework for Array Programs. ATVA (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Acceleration-based safety decision procedure for programs with arrays. LPAR (short papers) (2013)
Nick Bezhanishvili, Silvio Ghilardi
Bounded Proofs and Step Frames. TABLEAUX (2013)
Alessandro Carioni, Silvio Ghilardi, Silvio Ranise
Automated Termination in Model-Checking Modulo Theories. Int. J. Found. Comput. Sci. 24 (2) (2013)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Definability of Accelerated Relations in a Theory of Arrays and Its Applications. FroCos (2013)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Abstraction and Acceleration in SMT-based Model-Checking for Array Programs CoRR (2013)
Silvio Ghilardi
From free algebras to proof bounds. TACL (2013)
Franz Baader, Silvio Ghilardi, Carsten Lutz
LTL over description logic axioms. ACM Trans. Comput. Log. 13 (3) (2012)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
Lazy Abstraction with Interpolants for Arrays. LPAR (2012)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
Reachability Modulo Theory Library. SMT@IJCAR (2012)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. IJCAR (2012)
Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. NASA Formal Methods (2012)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
Quantifier-Free Interpolation of a Theory of Arrays Log. Methods Comput. Sci. 8 (2) (2012)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation CoRR (2012)
Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi
Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories. J. Satisf. Boolean Model. Comput. 8 (1/2) (2012)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
SAFARI: SMT-Based Abstraction for Arrays with Interpolants. CAV (2012)
Alessandro Carioni, Silvio Ghilardi, Silvio Ranise
Automated Termination in Model Checking Modulo Theories. RP (2011)
Franz Baader, Silvio Ghilardi
Unification in modal and description logics. Log. J. IGPL 19 (6) (2011)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. RTA (2011)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints. FroCoS (2011)
Guram Bezhanishvili, Silvio Ghilardi, Mamuka Jibladze
An Algebraic Approach to Subframe Logics. Modal Case. Notre Dame J. Formal Log. 52 (2) (2011)
Silvio Ghilardi
Book Reviews. Stud Logica 95 (3) (2010)
Silvio Ghilardi, Silvio Ranise
MCMT: A Model Checker Modulo Theories. IJCAR (2010)
Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi
Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems: a case study. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 35 (2010)
Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi
Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - A Case Study. DISC (2010)
Silvio Ghilardi, Silvio Ranise
Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis Log. Methods Comput. Sci. 6 (4) (2010)
Alessandro Carioni, Silvio Ghilardi, Silvio Ranise
MCMT in the Land of Parametrized Timed Automata. VERIFY@IJCAR (2010)
Silvio Ghilardi, Viorica Sofronie-Stokkermans, Ulrike Sattler, Ashish Tiwari
Special issue on automated deduction: Decidability, complexity, tractability. J. Symb. Comput. 45 (2) (2010)
Silvio Ghilardi
Continuity, freeness, and filtrations. J. Appl. Non Class. Logics 20 (3) (2010)

Silvio Ghilardi.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Silvio Ghilardi