SILVIO   GHILARDI

  Department of Mathematics - Università degli Studi di Milano

  via C. Saldini 50 - 20133 Milano - Italy

  tel. +39/0250316142 - e-mail: silvio.ghilardi@unimi.it

My research activity is mainly devoted to the integration of methods, topics and results coming from different areas of mathematical logic. Research interests include: modal logics, description logics, categorical and algebraic logic, automated reasoning, and model-checking. A full list of my publications is available (here).

Recent Publications (since 2000):

a) Journal Papers:

  1. S. Ghilardi, A. Gianola, D. Kapur, C. Naso Interpolation Results for Arrays with Length and MaxDiff, ACM Transactions on Computational Logic, to appear;
  2. N. Bezhanishvili, L. Carai, S. Ghilardi, L. Landi Admissibility of Π2-Inference Rules: interpolation, model completion, and contact algebras, Annals of Pure and Applied Logic, 174(1), 103169, (2023);
  3. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Combination of Uniform Interpolants via Beth Definability, Journal of Automated Reasoning, 66(3), pp. 409–435, (2022)
  4. S. Ghilardi, A. Gianola, D. Kapur Uniform Interpolants in EUF: Algorithms using DAG-representations, Logical Methods in Computer Science, 18(2), (2022);
  5. S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Petri Net-Based Object-Centric Processes with Read-Only Data, Information Systems, 127, 102011, (2022);
  6. S. Ghilardi, A. Gianola Interpolations and Uniform Interpolation in Quantifier-Free Fragments of Combined First Order Theories, Mathematica, 10(3), 461, Special Issue on ''Decidability of Logics and Their Theories and Combinations'', (invited contribution), (2022);
  7. S. Ghilardi, G. Lenzi Unification in Lax Logic, J. of Algebraic Hyperstructures and Logical Algebras, Special issue for 75th Birthday of A. di Nola, vol.3, n.1, pp. 61-76, (2022).
  8. D. Bruschi, A. Di Pasquale, S. Ghilardi, A. Lanzi, E. Pagani A formal verification of ARPON – a tool for avoiding Man-in-the-Middle attacks in Ethernet networks, Transactions on Dependable and Secure Computing, 19(6), pp. 4082–4098, (2022).
  9. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Model Completeness, Uniform Interpolants and Superposition Calculus (with Applications to Verification of Data-Aware Processes), Journal of Automated Reasoning, 65(7), pp. 941–969, (2021).
  10. G. Bezhanishvili, N. Bezhanishvili, L. Carai, D. Gabelaia, S. Ghilardi, M. Jibladze Diego's Theorem for nuclear implicative semilattices, Indagationes Mathematicae, 32(2), pp. 498-535, (2021).
  11. S. Ghilardi, E. Pagani Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems, Journal of Automated Reasoning, to appear.
  12. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin SMT-based Verification of Data-Aware Processes: a Model-Theoretic Approach, Mathematical Structures in Computer Science, 30(3): 271-313 (2020).
  13. S. Ghilardi, L. Santocanale Free Heyting Algebra Endomorphisms: Ruitenburg's Theorem and Beyond, Mathematical Structures in Computer Science, 30(6), pp. 572-596, (2020).
  14. L. Carai, S. Ghilardi Existentially Closed Browverian Semilattices, Journal of Symbolic Logic, 84(4): 1544-1575 (2019) (see the preliminary ArXiv version below).
  15. S. Ghilardi, M. J. Gouveia, L. Santocanale Fixed-point elimination in the Intuitionistic Propositional Calculus, ACM Transactions on Computational Logic, 21(1):1--37, (2019).
  16. S. Ghilardi, A. Gianola Modularity Results for Interpolation, Amalgamation and Superamalgamation, Annals of Pure and Applied Logic, pp.731-754 (2018).
  17. F. Alberti, S. Ghilardi, E. Pagani Cardinality Constraints for Arrays (decidability results and applications), Formal Methods in System Design, pp.545-574, (2017).
  18. N. Bezhanishvili, S. Ghilardi, F. Moellestrom Lauridsen One-Step Heyting Algebras and Hypersequent Calculi with the Bounded Proof Property, Journal of logic and Computation, pp.2135-2169 (2017).
  19. S. Ghilardi, S. van Gool A model-theoretic characterization of monadic second-order logic on infinite words, Journal of Symbolic Logic, Volume 82, Issue 1, pp. 62-76 (2017). A preliminary version is available here.
  20. N. Bezhanishvili, D. Gabelaia, S. Ghilardi, and M. Jibladze Admissible bases via stable canonical rules, Studia Logica, vol. 104(2), pp.317-341, (2016).
  21. F. Alberti, S. Ghilardi, N. Sharygina A framework for the verification of parameterized infinite-state systems, Fundamenta Informaticae, vol.150, pp.1-24, (2017).
  22. F. Alberti, S. Ghilardi, N. Sharygina Decision Procedures for Flat Array Properties, Journal of Automated Reasoning, vol. 54, n.4, pp.327-352, Springer, (2015).
  23. N. Bezhanishvili, S. Ghilardi, The bounded proof property via step algebras and step frames, Annals of Pure and Applied Logic, 165(12): 1832-1863 (2014).
  24. F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, N. Sharygina An extension of Lazy Abstraction with Interpolation for programs with arrays, Formal Methods in System Design 45(1): 63-109, Springer, (2014).
  25. S. Ghilardi, G. Mints The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination, Logic Journal of the IGPL 22(4): 585-596 (2014).
  26. R. Bruttomesso, S. Ghilardi, S. Ranise Quantifier-Free Interpolation in Combinations of Equality Interpolating Theories, ACM Transactions in Computational Logic, 15(1):5, 2014 (pdf).
  27. A. Carioni, S. Ghilardi, S. Ranise Automated Termination in Model Checking Modulo Theories, Int. J. of Foundations of Computer Science, vol. 24, n.2, pp.211-232, February 2013.
  28. R. Bruttomesso, S. Ghilardi, S. Ranise Quantifier-free Interpolation of a Theory of Arrays, Logical Methods in Computer Science, 8:2(2012 Apr), pp. 1-39 (link to the online paper).
  29. F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, G. Rossi Universal guards, relativization of quantifiers, and failure models in model checking modulo theories, Journal on Satisfiability, Boolean Modeling and Computation (JSAT), (file .pdf), vol. 8, p. 29-61, 2012.
  30. F. Baader, S. Ghilardi, C. Lutz LTL over Description Logic Axioms, ACM Transactions on Computational Logic, 13:3(2012 Aug), pp. 21.1-21.32, (pdf).
  31. G. Bezhanishvili, S. Ghilardi, M. Jibladze An algebraic approach to subframe logics. Modal case, Notre-Dame Journal of Formal Logic, vol. 52, n.2, 2011, (preliminary version).
  32. S. Ghilardi Continuity, Freeness, and Filtrations, Journal of Applied Non Classical Logics, vol.20, n.3, pp.193-217 (2010) (see the Technical report below for a preliminary version of the paper).
  33. S. Ghilardi, S. Ranise Backward Reachability of Array-based Systems by SMT Solving: Termination and Invariant Synthesis, Logical Methods in Computer Science, vol.6, n.4, 2010, link to the online paper.
  34. F. Baader, S. Ghilardi Unification in Modal and Description Logics, Logic Journal of the IGPL, vol.19, n.6, pp. 705-730, 2011.
  35. S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli Decision Procedures for Extensions of the Theory of Arrays, Annals of Mathematics and Artificial Intelligence, 50(3-4), pp.231-254, (2007).
  36. S. Ghilardi, E. Nicolini, D. Zucchelli A Comprehensive Combination Framework, ACM Transactions on Computational Logic , vol.9(2), pp.1-54 (2008).
  37. G. Bezhanishvili, S. Ghilardi An Algebraic Approach to Subframe Logics. Intuitionistic Case, Annals of Pure and Applied Logic, vol. 147, pp. 84-100, (2007).
  38. F. Baader, S. Ghilardi Connecting Many-Sorted Theories , Journal of Symbolic Logic, vol. 72, n.2, pp. 535-583, (2007).
  39. F. Baader, S. Ghilardi, C. Tinelli A New Combination Procedure for the Word Problem that generalizes Fusion Decidability in Modal Logic , Information and Computation, vol.204, issue 10, pp.1413-1452 (2006).
  40. S. Ghilardi Model Theoretic Methods in Combined Constraint Satisfiability, Journal of Automated Reasoning, vol. 33, no. 3-4, pp.221-249 (2005). (preliminary version, file .pdf)
  41. S, Ghilardi, L. Sacchetti Filtering Unification and Most General Unifiers in Modal Logic, Journal of Symbolic Logic, 69, 3, pp.879-906 (2004).
  42. S. Ghilardi Unification, Finite Duality and Projectivity in Locally Finite Varieties of Heyting Algebras , Annals of Pure and Applied Logic, vol. 127/1-3, pp.99-115 (2004).
  43. C. Fiorentini, S. Ghilardi Combining Word Problems Through Rewriting in Categories with Products, Theoretical Computer Science, 294, pp. 103-149 (2003).
  44. S. Ghilardi A resolution/tableaux algorithm for projective approximations in IPC, Logic Journal of the IGPL, vol.10, n.3, pp.227-241 (2002).
  45. S. Ghilardi Best solving modal equations, Annals of Pure and Applied Logic, 102, pp.183-198 (2000).

b) Books and Book Chapters:

  1. S. Ghilardi The invariance modality, in Citkin, Vandoulakis (eds.) "V.A. Jankov on Non-Classivcal Logics, History and Philosophy of Mathematics", Outstanding Contributions to Logic, 24, pp. 165–175, (2022);
  2. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin From Model Completeness to Verification of Data Aware Processes, in "Description Logics, Theory Combinations, and All That", Springer Festschtift, LNCS 11560, pp.212-239, (2019).
  3. A. Cimatti, S. Ghilardi, S. Ranise Model Checking: teoria ed applicazioni, in ``Direzioni della ricerca logica in Italia'', vol. II, to appear.
  4. W. Conradie, S. Ghilardi, and A. Palmigiano Unified Correspondence, J. van Benthem on Logic and Information Dynamics, edited by A. Baltag and S. Smets, Outstanding Contributions to Logic, pp. 933-976, Springer, (2014).
  5. N. Bezhanishvili, S. Ghilardi, and M. Jibladze Free modal algebras revisited: the step-by-step method, in "Leo Esakia on Duality in Modal and Intuitionistic Logics", Outstanding Contributions to Logic, Springer, pp.43-62, (2014).
  6. T. Brauner, S. Ghilardi First Order Modal Logic, in P. Blackburn, J. van Benthem, F. Wolter (eds.), ''Handbook of Modal Logic'', Elsevier, pp.549-620, (2007).
  7. S. Ghilardi, E. Nicolini, D. Zucchelli Recent Advances in Combined Decision Problems, in E. Ballo, M. Franchella (eds.) ``Logic and Philosophy in Italy: Trends and Perspectives (Essays in Honor of C. Mangione)'', Polimetrica, Milano, (2006).
  8. S.Ghilardi, ''Sfidare l'Indecidibile (tecniche e metodologie del ragionamento automatico nella logica elementare con identità)'', Polimetrica, 2004; thanks to the publisher permission, the pdf file of the book is made available (here).
  9. S.Ghilardi, M. Zawadowski Sheaves, Games and Model Completions (a categorical approach to non classical propositional logics), Trends in Logic Series, Kluwer (2002).
  10. S. Ghilardi, M. Zawadowski From bisimulation quantifiers to classifying toposes, in F. Wolter, M. de Rijke, H. Wansing, M. Zakharyaschev (eds.) 'Advances in Modal Logic, vol. III', World Scientific Publ., pp.193-220 (2002).
  11. S. Ghilardi Substitution, quantifiers and identity in modal logic, in Hieke A. - Morscher E. (eds.) ``New Essays in Free Logic (in honour of K. Lambert)'', Applied Logic Series, vol.23, pp.87-115, Kluwer (2001).

c) Conference/Workshop Papers:

  1. S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Safety Verification and Universal Invariants for Relational Action Bases, Proc. of the 32nd Int. Joint Conf. on Artificial Intelligence (IJCAI 23), to appear.
  2. J. Abel Castellanos Joo, S. Ghilardi, A. Gianola, D. Kapur AXD Interpolator: a Tool for Computing Interpolants for Arrays with MaxDiff, Proc. of SMT Workshop 2021, Easy Chair Conf. Proc., to appear.
  3. S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Delta-BPMN: a Concrete Language and Verifier for Data-aware BPMN, Proc. of BPM 2021, Springer LNCS, to appear.
  4. S. Ghilardi, A. Gianola, D. Kapur Interpolation and Amalgamation for Arrays with MaxDiff, Proc. of FoSSaCS 2021, Springer LNCS, to appear.
  5. S. Ghilardi, A. Gianola, D. Kapur Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations, Proc. of CILC 2020, CEUR Workshop Proceedings, vol.2710, pp.67-81 (2020).
  6. N. Bezhanishvili, S. Ghilardi, L. Landi Model Completeness and Π_2-rules: the case of Contact Algebras, Proc. of AiML 2020, College Publications, (2020).
  7. S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Petri Nets with Parameterised Data: Modelling and Verification, Proc. of BPM 2020, Springer LNCS n.12168, pp. 55-74 (2020).
  8. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Combined Covers and Beth Definability, Proc. of IJCAR 2020, Springer LNAI n. 12166, pp. 181-200, (2020).
  9. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Verification of data-aware processes: Challenges and opportunities for automated reasoning, Proc. of ARCADE 19, EPTCS, 2019.
  10. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN, Proc. of BPM 19, Springer LNCS, 2019.
  11. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Model Completeness, Covers and Superposition, Proc. of CADE, Springer LNCS, 2019; the extended version is available here.
  12. S. Ghilardi, L. Santocanale Ruitenburg's Theorem via Duality and Bounded Bisimulations, Proceedings of AiML, 2018, College Publications.
  13. S. Ghilardi, E. Pagani Second Order Quantifier Elimination: Towards Verification Applications, Proc. of the Workshop on Second Order Quantifier Elimination (SOQE 17), CEUR; the extended version is available here.
  14. S. Ghilardi, E. Pagani Counter Simulations via Higher Order Quantifier Elimination: a preliminary report, Proc. of the Fifth Workshop on Proof eXchange for Theorem Proving (PxTP 17), EATCS; the preliminary workshop version is available here.
  15. S. Ghilardi, A. Gianola Interpolation, Amalgamation and Combination (the non-disjoint signatures case), Proceedings of FroCoS 2017, Springer LNAI; a larger manuscript covering the paper's content is available here. The original publication is available at www.springerlink.com.
  16. D. Bruschi, A. Di Pasquale, S. Ghilardi, A. Lanzi, and E. Pagani Formal verification of ARP (Address Resolution Protocol) through SMT-based model checking - A case study, Proc. of iFM ("Integrated Formal Methods"), Springer LNCS, 2017, (file .pdf). The original publication is available at www.springerlink.com.
  17. M. Bersani, M. Erascu, S. Ghilardi, F. Marconi, M. Rossi Formal Verification of Data-Intensive Applications through Model Checking Modulo Theories, Proc. of SPIN 2017, (file .pdf).
  18. S. Ghilardi, S. van Gool Monadic second order logic as the model companion of temporal logic, Proceedings of LICS, 2016 (extended version, file .pdf).
  19. F. Alberti, S. Ghilardi, E. Pagani Counting constraints in flat array fragments, Proceedings of IJCAR, Springer LNAI, vol. 9706, pp.65-81, 2016. A preliminary version is available here.
  20. F. Alberti, S. Ghilardi, A. Orsini, E. Pagani Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies, Proc. of CILC 2016, CEUR, pp.102-117, 2016. (file .pdf)
  21. S. Ghilardi, M. J. Gouveia, L. Santocanale Fixed-point elimination in the Intuitionistic Propositional Calculus, Proceedings of FoSSaCS, 2016, Springer LNCS, pp. 126-141. (file .pdf). The original publication is available at www.springerlink.com.
  22. F. Alberti, S. Ghilardi, N. Sharygina A new Acceleration-based Combination Framework for Array Properties, Proceedings of FroCoS 2015, pp.169-185, 2015. (extended version, file .pdf). The original publication is available at www.springerlink.com.
  23. F. Alberti, S. Ghilardi, N. Sharygina Monotonic Abstraction Techniques: from Parametric to Software Model Checking, Proceedings of MOD*, EPTCS 168, pp.1-11, 2014.
  24. F. Alberti, S. Ghilardi, N. Sharygina Booster: an acceleration-based verification framework for array programs, Proceedings of ATVA 2014, pp.18-23, Springer LNCS, 2014 (file .pdf). The original publication is available at www.springerlink.com.
  25. N. Bezhanishvili, S. Ghilardi Multiple-conclusion Rules, Hypersequents Syntax and Step Frames, Advances in Modal Logic 2014: 54-73, College Publications, 2014. (extended TR version .pdf).
  26. F. Alberti, S. Ghilardi, N. Sharygina A framework for the verification of parameterized infinite-state systems, Proceedings of CILC 2014, pp.303-308, CEUR, 2014. (file .pdf).
  27. F. Alberti, S. Ghilardi, N. Sharygina Decision Procedures for Flat Array Properties , Proceedings of TACAS 2014, Springer LNCS, pp.15-30, (file .pdf). The original publication is available at www.springerlink.com.
  28. N. Bezhanishvili, S. Ghilardi Bounded Proofs and Step Frames, Proceedings of Tableaux 2013, Springer LNAI, (file .pdf). The original publication is available at www.springerlink.com.
  29. F. Alberti, S. Ghilardi, N. Sharygina Definability of Accelerated Relations in a Theory of Arrays and its Applications, Proceedings of FroCoS 2013, Springer LNAI, (file .pdf). The original publication is available at www.springerlink.com.
  30. R. Bruttomesso, S. Ghilardi, S. Ranise From Strong Amalgamation to Modularity of Quantifier-Free Interpolation, Proc. of IJCAR 2012, Springer LNAI, vol.7364, pp.118-133 (file .pdf). The original publication is available at www.springerlink.com.
  31. F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, N. Sharygina SAFARI: SMT-based Abstraction For Arrays with Interpolants, Proceedings of CAV 2012, Springer LNCS, vol.7180, pp.46-61 (2012); (file.pdf). The original publication is available at www.springerlink.com.
  32. R. Bruttomesso, A. Carioni, S. Ghilardi, S. Ranise Automated Analysis of Parametric Timing Based Mutual Exclusion Protocols, Proceedings of the Fourth NASA Formal Methods Symposium, Springer LNCS, vol. 7226, pp. 279-294 (2012); [pdf of extended version]. The original publication is available at www.springerlink.com.
  33. F. Alberti, R. Bruttomesso, S, Ghilardi, S. Ranise, N. Sharygina Lazy Abstraction with Interpolants for Arrays, Proceedings of LPAR-18, Springer LNCS, vol.7180, pp.46-61 (2012); an extended version is available here. The original publication is available at www.springerlink.com.
  34. R. Bruttomesso, S. Ghilardi, S. Ranise A Combination of Rewriting and Constraint Solving for the Quantifier-free Interpolation of Arrays with Integer Difference Constraints, Proc. of the VIII Int. Symp. on Frontiers on Combining Systems (FroCoS '11), Springer LNAI, vol. 6989, pp. 103-118, 2011, (file .pdf); an extended version is available here. The original publication is available at www.springerlink.com.
  35. A. Carioni, S. Ghilardi, S. Ranise Automated Termination in Model Checking Modulo Theories, Proc. of the 5th Int. Workshop on Reachability Problems (RP 11), Springer LNCS, vol. 6945, pp. 110-124, (file.pdf), 2011. The extended version is available as a Technical Report here. The original publication is available at www.springerlink.com.
  36. R. Bruttomesso, S. Ghilardi, S. Ranise Rewriting-based Quantifier-free Interpolation for a Theory of Arrays, Proc. of the 22nd Int. Conf. on Rewriting Techniques and Applications (RTA '11), Leibniz Int. Proc. in Informatics, Dagstuhl Publishing, vol. 10, pp. 171-186, 2011 (file .pdf); an extended version is available as a Technical Report here.
  37. F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, G. Rossi Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - a case study , Proc. of the 10th Int. Work. on Automated Verification of Critical Systems (AVOCS 10), Electr. Communications of the EASST, vol.X, (file.pdf of the preliminary conference version), 2010.
  38. F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, G. Rossi Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - a case study , Proc. of the XXIV DIStributed Computing Conference (DISC 10), Springer LNCS, (file.pdf), 2010. The original publication is available at www.springerlink.com.
  39. A. Carioni, S. Ghilardi, S. Ranise MCMT in the Land of Parameterized Timed Automata, In Proc. of VERIFY 2010, co-located with IJCAR, Edinburgh, (2010), (file.pdf).
  40. S. Ghilardi, S. Ranise MCMT: a Model Checker Modulo Theories (system description), Proc. of the 5th International Joint Conference on Automated Reasoning (IJCAR 10), Springer LNAI, vol. 6173, pp. 22-29, (file.pdf), 2010. The original publication is available at www.springerlink.com.
  41. S. Ghilardi, S. Ranise Model Checking Modulo Theory at work: the intergration of Yices in MCMT, In Proc. of AFM 09, Grenoble, ACM Digital Library, to appear (2009), (file.pdf).
  42. S. Ghilardi, S. Ranise Goal Directed Invariant Synthesis for Model Checking Modulo Theories, Proc. of the 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 09),Springer LNAI, vol.5607, pp.173-188 (2009), (file.pdf).
  43. S. Ghilardi, S. Ranise, T. Valsecchi Light-Weight SMT-based Model Checking, 8th Int. Work. on Automated Verification of Critical Systems (AVOCS 08), Glasgow, (2008), Electr. Notes in Theor. Comp. Sci., to appear, (2008), (file.pdf), (extended version file.pdf)).
  44. F. Baader, S. Ghilardi, C. Lutz LTL over Description Logics Axioms, 11th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 08), pp.684-694, (2008), (file.pdf).
  45. S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli Towards SMT Model-Checking of Array-based Systems, Proceedings of the IV Int. Joint Conf. on Automated Reasoning (IJCAR 08), Springer LNAI, vol.5195, pp.67-82, (2008), (file.pdf).
  46. F. Baader, S. Ghilardi, C. Lutz LTL over Description Logic Axioms, "21st International Workshop on Description Logics" (DL08), Oral Presentation, Dresden, (2008).
  47. S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli Noetherianity and Combination Problems, Proceedings of the VI International Symposium on Frontiers of Combining Systems (FroCoS 07), Lecture Notes in Artificial Intelligence, vol.4720, pp.206-220, Springer, (2007) (follow this link to download the paper).
  48. S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems, Proceedings of the 21-th Conference on Automated Deduction (CADE-21), Lecture Notes in Artificial Intelligence, vol.4603, pp.362-378, Springer, (2007) (follow this link to download the paper).
  49. S. Ghilardi, C. Lutz, F. Wolter, M. Zakharyaschev Conservative Extensions in Modal Logic, Proceedings of "Advances in Modal Logic (AiML 06)", College Publications, pp.187-207, (2006) (follow this link to download the paper).
  50. S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies. Proceedings of the 10th European Conference on Logic in Artificial Intelligence (JELIA 06), Springer Lecture Notes in Artificial Intelligence, vol.4160, pp.177-189, (follow this link to download the paper).
  51. M. P. Bonacina, S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli Decidability and Undecidability Results for Nelson-Oppen and Rewrite-based Decision Procedures, Proceedings of the "Third International Joint Conference on Automated Reasoning (IJCAR 06)", Springer Lecture Notes in Artificial Intelligence, vol.4130, pp.513-527, (follow this link to download the paper).
  52. S. Ghilardi, C. Lutz, F. Wolter Did I damage my Ontology ?, Proceedings of Principles of Knowledge Representation and Reasoning 2006 (KR06), AAAI Press, pp.187-197 (follow this link to download both the paper and the full version).
  53. F. Baader, S. Ghilardi Connecting many-sorted structures and theories through adjoint functions , Proceedings of the Fifth International Workshop on Frontiers of Combining Systems (FroCoS 05), Lecture Notes in Artificial Intelligence, Springer, vol. 3717, pp. 31-47, (2005). (file .pdf)
  54. F. Baader, S. Ghilardi Connecting many-sorted theories , Proceedings of the Twentieth Conference on Automated Deduction (CADE-20), Lecture Notes in Artificial Intelligence, Springer, to app. (2005). (file .pdf)
  55. S. Ghilardi, E. Nicolini, D. Zucchelli A Comprehensive Framework for Combining Decision Procedures , Proceedings of the Fifth International Workshop on Frontiers of Combining Systems (FroCoS 05), Lecture Notes in Artificial Intelligence, Springer, vol. 3717, vol. 3717, pp. 1-30, (2005). (file .pdf)
  56. F. Baader, S. Ghilardi, C. Tinelli A New Combination Procedure for the Word Problem that generalizes Fusion Decidability in Modal Logic , Proc. of the Second Int. Joint Conference on Automated Reasoning (IJCAR 04), Springer LNAI 3097, pp. 183-197 (2004). (file .pdf)
  57. S. Ghilardi, L. Santocanale Algebraic and Model-Theoretic Techniques for Fusion Decidability in Modal Logic, in Vardi M., Voronkov A. ``Logic for Programming, Artificial Intelligence and Reasoning (LPAR 03)'' Springer LNAI, vol.2850, pp.152-166 (2003). (file .pdf)
  58. S. Ghilardi Quantifier Elimination and Provers' Integration, Proceedings of FTP (First Order Theorem Proving) 03, Electronic Notes in Theoretical Computer Science 86, n.1 (2003). (file .pdf)

d) Some Technical Reports/Drafts:

  1. S. Ghilardi, L. Santocanale Free Heyting Algebra Endomorphisms: Ruitenburg's Theorem and Beyond, HAL preprint, available here, January 2019.
  2. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Verification of Data-Aware Processes via Array-Based Systems, ArXiv preprint, available here.
  3. D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Quantifier Elimination for Database Driven Verification, ArXiv preprint, available here.
  4. S. Ghilardi, L. Santocanale Ruitenburg's Theorem via Duality and Bounded Bisimulations, ArXiv and HAL preprint, available here or here.
  5. L. Carai, S. Ghilardi Existentially Closed Brouwerian Semilattices, ArXiv preprint, revised version, July 2017, available here.
  6. S. Ghilardi, M. J. Gouveia, L. Santocanale Fixed-point elimination in the Intuitionistic Propositional Calculus, January 2016, HAL preprint, available here.
  7. F. Alberti, S. Ghilardi, N. Sharygina Decision Procedures for Flat Array Properties, Technical Report USI-INF-TR-2013-04, Università della Svizzera Italiana, 2013. (pdf).
  8. N. Bezhanishvili, S. Ghilardi Bounded Proofs and Step Frames, Logic Group Preprint Series, n.306, (2013), Utrecht University (file.pdf)
  9. N. Bezhanishvili, S. Ghilardi, and M. Jibladze Free modal algebras revisited: the step-by-step method, Logic Group Preprint Series, n.302, (2012), Utrecht University (pdf).
  10. F. Alberti, S. Ghilardi, N. Sharygina Abstraction and Acceleration in SMT-based Model-Checking for Array Programs, Technical Report USI-INF-TR-2012-1, Università della Svizzera Italiana, 2012. (pdf).
  11. R. Bruttomesso, S. Ghilardi, S. Ranise From Strong Amalgamability to Modularity of Quantifier-free Interpolation, Rapporto Interno 337-12, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, (2012), (pdf).
  12. A. Carioni, S. Ghilardi, S. Ranise Automated Termination in Model Checking Modulo Theories- extended version, Rapporto Interno 336-11, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, (2011), (pdf).
  13. R. Bruttomesso, S. Ghilardi, S. Ranise Rewriting-based Quantifier-free Interpolation for a Theory of Array (extended version), Rapporto Interno 334-10, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, (2011), (pdf).
  14. S. Ghilardi Continuity, Freeness, and Filtrations, Rapporto Interno 331-10, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, (2010), (pdf).
  15. S. Ghilardi, S. Ranise Goal Directed Invariant Synthesis in Model Checking Modulo Theories, Rapporto Interno 325-09, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, (2009), (pdf).
  16. S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli Towards SMT Model-Checking of Array-based systems, Rapporto Interno 318-08, Dipartimento di Scienze dell'informazione, Università degli Studi di Milano, (2008), (pdf).
  17. F. Baader, S. Ghilardi, C. Lutz LTL over description logic axioms, LTCS Report-08-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, (2008), (pdf).
  18. S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems, Rapporto Interno 313-07, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, (2007), (pdf).
  19. S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies. Rapporto Interno 309-06, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, Milano (Italy), 2006, (pdf).
  20. M. P. Bonacina, S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli Decidability and Undecidability Results for Nelson-Oppen and Rewrite-based Decision Procedures, Rapporto Interno n. 308-06, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, (2006) (file .pdf)
  21. S. Ghilardi, E. Nicolini, D. Zucchelli A Comprehensive Framework for Combining Decision Procedures , Rapporto Interno n. 304-05, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, (2005). (follow this link to download the paper).
  22. F. Baader, S. Ghilardi Connecting many-sorted Theories , LTCS Report 05-04, Technische Universitaet Dresden, (2005) (follow this link to download the paper).
  23. F. Baader, S. Ghilardi, C. Tinelli A New Combination Procedure for the Word Problem that generalizes Fusion Decidability in Modal Logic , Technical Report No. 03-03, Department of Computer Science, The University of Iowa (2003) (follow this link to download the paper).
  24. S. Ghilardi Reasoners' Cooperation and Quantifier Elimination, Rapporto Interno n. 288-03, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, (2003). (file .ps)
  25. C. Fiorentini, S. Ghilardi Path rewriting and Combined Word Problems, Rapporto Interno n.250-00, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, (2000). (file .pdf)

e) Edited Volumes/Special Issues/Journals:

  1. S. Ghilardi, D. Mundici, Constructivism in Non-Classical Logics and in Computer Science - In Memoriam P. Miglioli, Studia Logica, Vol.73, N.1, (2003).
  2. S. Ghilardi, R. Sebastiani, Frontiers of Combining Systems, 7th International Symposium (FroCoS 2009), Springer LNAI 5749, (2009).
  3. S. Ghilardi, V. Sofronie-Stokkermans, U. Sattler, A. Tiwari, Special issue on automated deduction: Decidability, complexity, tractability, J. Symb. Comput. 45(2): 151-152 (2010).
  4. T. Bolander, T. Brauner, S. Ghilardi, L. Moss, Advances in Modal Logic IX, College Publications (2012).
  5. I am associate editor of the Journal of Automated Reasoning.
  6. I am editor of the Review of Symbolic Logic.

Tools:

Some Slides:

Events: