| 2024 | AiML | Unification With Simple Variable Restrictions and Admissibility of Π2-Rules. | Rodrigo Nicolau Almeida, Silvio Ghilardi |
| 2024 | IJCAR | Model Completeness for Rational Trees. | Silvio Ghilardi, Lia M. Poidomani |
| 2023 | IJCAI | Safety Verification and Universal Invariants for Relational Action Bases. | Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin |
| 2021 | BPM | Delta-BPMN: A Concrete Language and Verifier for Data-Aware BPMN. | Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin |
| 2021 | FOSSACS | Interpolation and Amalgamation for Arrays with MaxDiff. | Silvio Ghilardi, Alessandro Gianola, Deepak Kapur |
| 2020 | AiML | Model Completeness and Π | Nick Bezhanishvili, Silvio Ghilardi, Lucia Landi |
| 2020 | BPM | Petri Nets with Parameterised Data - Modelling and Verification. | Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin |
| 2020 | CADE | Combined Covers and Beth Definability. | Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin |
| 2019 | BPM | Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN. | Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin |
| 2019 | CADE | Model Completeness, Covers and Superposition. | Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin |
| 2018 | AiML | Ruitenburg's Theorem via Duality and Bounded Bisimulations. | Silvio Ghilardi, Luigi Santocanale |
| 2017 | IFM | Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study -. | Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi, Elena Pagani |
| 2016 | CADE | Counting Constraints in Flat Array Fragments. | Francesco Alberti, Silvio Ghilardi, Elena Pagani |
| 2016 | FOSSACS | Fixed-Point Elimination in the Intuitionistic Propositional Calculus. | Silvio Ghilardi, Maria Joo Gouveia, Luigi Santocanale |
| 2016 | LICS | Monadic second order logic as the model companion of temporal logic. | Silvio Ghilardi, Sam van Gool |
| 2014 | AiML | Multiple-conclusion Rules, Hypersequents Syntax and Step Frames. | Nick Bezhanishvili, Silvio Ghilardi |
| 2014 | ATVA | Booster: An Acceleration-Based Verification Framework for Array Programs. | Francesco Alberti, Silvio Ghilardi, Natasha Sharygina |
| 2014 | TACAS | Decision Procedures for Flat Array Properties. | Francesco Alberti, Silvio Ghilardi, Natasha Sharygina |
| 2013 | LPAR | Acceleration-based safety decision procedure for programs with arrays. | Francesco Alberti, Silvio Ghilardi, Natasha Sharygina |
| 2013 | TABLEAUX | Bounded Proofs and Step Frames. | Nick Bezhanishvili, Silvio Ghilardi |
| 2012 | CADE | Reachability Modulo Theory Library. | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina |
| 2012 | CADE | From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. | Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise |
| 2012 | CAV | SAFARI: SMT-Based Abstraction for Arrays with Interpolants. | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina |
| 2012 | LPAR | Lazy Abstraction with Interpolants for Arrays. | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina |
| 2010 | CADE | MCMT in the Land of Parametrized Timed Automata. | Alessandro Carioni, Silvio Ghilardi, Silvio Ranise |
| 2010 | CADE | MCMT: A Model Checker Modulo Theories. | Silvio Ghilardi, Silvio Ranise |
| 2009 | TABLEAUX | Goal-Directed Invariant Synthesis for Model Checking Modulo Theories. | Silvio Ghilardi, Silvio Ranise |
| 2008 | CADE | Towards SMT Model Checking of Array-Based Systems. | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
| 2008 | KR | LTL over Description Logic Axioms. | Franz Baader, Silvio Ghilardi, Carsten Lutz |
| 2007 | CADE | Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
| 2006 | AiML | Conservative extensions in modal logic. | Silvio Ghilardi, Carsten Lutz, Frank Wolter, Michael Zakharyaschev |
| 2006 | CADE | Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures. | Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
| 2006 | JELIA | Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies. | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
| 2006 | KR | Did I Damage My Ontology? A Case for Conservative Extensions in Description Logics. | Silvio Ghilardi, Carsten Lutz, Frank Wolter |
| 2005 | CADE | Connecting Many-Sorted Theories. | Franz Baader, Silvio Ghilardi |
| 2004 | CADE | A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics. | Franz Baader, Silvio Ghilardi, Cesare Tinelli |
| 2003 | LPAR | Algebraic and Model Theoretic Techniques for Fusion Decidability in Modal Logics. | Silvio Ghilardi, Luigi Santocanale |
| 2000 | AiML | From Bisimulation Quantifiers to Classifying Toposes. | Silvio Ghilardi, Marek W. Zawadowski |