default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSilvio Ghilardi
Person information
- affiliation: University of Milan, Italy
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j61]Matteo De Berardinis, Silvio Ghilardi
:
Profiniteness, monadicity and universal models in modal logic. Ann. Pure Appl. Log. 175(7): 103454 (2024)- [c65]Rodrigo Nicolau Almeida, Silvio Ghilardi:
Unification With Simple Variable Restrictions and Admissibility of Π2-Rules. AiML 2024: 79-100 - [c64]Silvio Ghilardi, Lia M. Poidomani:
Model Completeness for Rational Trees. IJCAR (1) 2024: 265-283 - [i21]Rodrigo Nicolau Almeida, Silvio Ghilardi:
Unification with Simple Variable Restrictions and Admissibility of Π2-rules. CoRR abs/2406.03265 (2024) - 2023
- [j60]Nick Bezhanishvili, Luca Carai, Silvio Ghilardi, Lucia Landi:
Admissibility of Π2-Inference Rules: interpolation, model completion, and contact algebras. Ann. Pure Appl. Log. 174(1): 103169 (2023) - [j59]Silvio Ghilardi, Alessandro Gianola, Deepak Kapur, Chiara Naso:
Interpolation Results for Arrays with Length and MaxDiff. ACM Trans. Comput. Log. 24(4): 28:1-28:33 (2023) - [c63]Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Safety Verification and Universal Invariants for Relational Action Bases. IJCAI 2023: 3248-3257 - 2022
- [j58]Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Petri net-based object-centric processes with read-only data. Inf. Syst. 107: 102011 (2022) - [j57]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Combination of Uniform Interpolants via Beth Definability. J. Autom. Reason. 66(3): 409-435 (2022) - [j56]Silvio Ghilardi, Alessandro Gianola, Deepak Kapur:
Uniform Interpolants in EUF: Algorithms using DAG-representations. Log. Methods Comput. Sci. 18(2) (2022) - [j55]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): 4082-4098 (2022) - [i20]Silvio Ghilardi, Alessandro Gianola, Deepak Kapur, Chiara Naso:
General Interpolation and Strong Amalgamation for Contiguous Arrays. CoRR abs/2204.11771 (2022) - [i19]Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version). CoRR abs/2208.06377 (2022) - 2021
- [j54]Silvio Ghilardi, Elena Pagani:
Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems. J. Autom. Reason. 65(3): 425-460 (2021) - [j53]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Model Completeness, Uniform Interpolants and Superposition Calculus. J. Autom. Reason. 65(7): 941-969 (2021) - [c62]Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Delta-BPMN: A Concrete Language and Verifier for Data-Aware BPMN. BPM 2021: 179-196 - [c61]Silvio Ghilardi, Alessandro Gianola, Deepak Kapur:
Interpolation and Amalgamation for Arrays with MaxDiff. FoSSaCS 2021: 268-288 - [c60]José Abel Castellanos Joo, Silvio Ghilardi, Alessandro Gianola, Deepak Kapur:
AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDiff. SMT 2021: 40-52 - 2020
- [j52]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): 271-313 (2020) - [j51]Silvio Ghilardi, Luigi Santocanale:
Free Heyting algebra endomorphisms: Ruitenburg's Theorem and beyond. Math. Struct. Comput. Sci. 30(6): 572-596 (2020) - [j50]Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale:
Fixed-point Elimination in the Intuitionistic Propositional Calculus. ACM Trans. Comput. Log. 21(1): 4:1-4:37 (2020) - [c59]Nick Bezhanishvili, Silvio Ghilardi, Lucia Landi:
Model Completeness and Π2-rules: The Case of Contact Algebras. AiML 2020: 115-132 - [c58]Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Petri Nets with Parameterised Data - Modelling and Verification. BPM 2020: 55-74 - [c57]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Combined Covers and Beth Definability. IJCAR (1) 2020: 181-200 - [c56]Silvio Ghilardi, Alessandro Gianola, Deepak Kapur:
Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations. CILC 2020: 67-81 - [i18]Silvio Ghilardi, Alessandro Gianola, Deepak Kapur:
Compactly Representing Uniform Interpolants for EUF using (conditional) DAGS. CoRR abs/2002.09784 (2020) - [i17]Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Petri Nets with Parameterised Data: Modelling and Verification (Extended Version). CoRR abs/2006.06630 (2020) - [i16]Silvio Ghilardi, Alessandro Gianola, Deepak Kapur:
Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version). CoRR abs/2010.07082 (2020)
2010 – 2019
- 2019
- [j49]Luca Carai, Silvio Ghilardi:
Existentially closed Brouwerian Semilattices. J. Symb. Log. 84(4): 1544-1575 (2019) - [c55]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: 212-239 - [c54]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN. BPM 2019: 157-175 - [c53]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Model Completeness, Covers and Superposition. CADE 2019: 142-160 - [c52]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Model Completeness, Covers and Superposition (Abridged Version). CILC 2019 - [i15]Silvio Ghilardi, Luigi Santocanale:
Free Heyting Algebra Endomorphisms: Ruitenburg's Theorem and Beyond. CoRR abs/1901.01252 (2019) - [i14]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN. CoRR abs/1905.12991 (2019) - [i13]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version). CoRR abs/1906.07811 (2019) - [i12]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Combined Covers and Beth Definability. CoRR abs/1911.07774 (2019) - 2018
- [j48]Silvio Ghilardi, Alessandro Gianola:
Modularity results for interpolation, amalgamation and superamalgamation. Ann. Pure Appl. Log. 169(8): 731-754 (2018) - [c51]Silvio Ghilardi, Luigi Santocanale:
Ruitenburg's Theorem via Duality and Bounded Bisimulations. Advances in Modal Logic 2018: 277-290 - [i11]Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale:
Fixed-point elimination in the Intuitionistic Propositional Calculus (extended version). CoRR abs/1803.01552 (2018) - [i10]Luigi Santocanale, Silvio Ghilardi:
Ruitenburg's Theorem via Duality and Bounded Bisimulations. CoRR abs/1804.06130 (2018) - [i9]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Quantifier Elimination for Database Driven Verification. CoRR abs/1806.09686 (2018) - [i8]Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin:
Verification of Data-Aware Processes via Array-Based Systems (Extended Version). CoRR abs/1806.11459 (2018) - 2017
- [j47]Francesco Alberti, Silvio Ghilardi, Elena Pagani:
Cardinality constraints for arrays (decidability results and applications). Formal Methods Syst. Des. 51(3): 545-574 (2017) - [j46]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
A Framework for the Verification of Parameterized Infinite-state Systems. Fundam. Informaticae 150(1): 1-24 (2017) - [j45]Silvio Ghilardi, Samuel J. van Gool:
A Model-Theoretic characterization of Monadic second order Logic on Infinite Words. J. Symb. Log. 82(1): 62-76 (2017) - [j44]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): 2135-2169 (2017) - [c50]Silvio Ghilardi, Alessandro Gianola:
Interpolation, Amalgamation and Combination (The Non-disjoint Signatures Case). FroCoS 2017: 316-332 - [c49]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: 391-406 - [c48]Silvio Ghilardi, Elena Pagani:
Second Order Quantifier Elimination: Towards Verification Applications. SOQE 2017: 36-50 - [c47]Marcello M. Bersani, Francesco Marconi, Matteo Rossi, Madalina Erascu, Silvio Ghilardi:
Formal verification of data-intensive applications through model checking modulo theories. SPIN 2017: 98-101 - [c46]Silvio Ghilardi, Elena Pagani:
Counter Simulations via Higher Order Quantifier Elimination: a preliminary report. PxTP 2017: 39-53 - 2016
- [j43]Nick Bezhanishvili, David Gabelaia, Silvio Ghilardi, Mamuka Jibladze:
Admissible Bases Via Stable Canonical Rules. Stud Logica 104(2): 317-341 (2016) - [c45]Francesco Alberti, Silvio Ghilardi, Elena Pagani:
Counting Constraints in Flat Array Fragments. IJCAR 2016: 65-81 - [c44]Francesco Alberti, Silvio Ghilardi, Andrea Orsini, Elena Pagani:
Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies. CILC 2016: 102-117 - [c43]Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale:
Fixed-Point Elimination in the Intuitionistic Propositional Calculus. FoSSaCS 2016: 126-141 - [c42]Silvio Ghilardi, Sam van Gool:
Monadic second order logic as the model companion of temporal logic. LICS 2016: 417-426 - [e3]Silvio Ghilardi, Manfred Schmidt-Schauß:
Proceedings of the 30th International Workshop on Unification, UNIF 2016, Porto, Portugal, June 26, 2016. 2016 [contents] - [i7]Silvio Ghilardi, Maria João Gouveia, Luigi Santocanale:
Fixed-point elimination in the intuitionistic propositional calculus. CoRR abs/1601.00402 (2016) - [i6]Francesco Alberti, Silvio Ghilardi, Elena Pagani:
Counting Constraints in Flat Array Fragments. CoRR abs/1602.00458 (2016) - [i5]Silvio Ghilardi, Samuel J. van Gool:
Monadic second order logic as the model companion of temporal logic. CoRR abs/1605.01003 (2016) - 2015
- [j42]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
Decision Procedures for Flat Array Properties. J. Autom. Reason. 54(4): 327-352 (2015) - [c41]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
A New Acceleration-Based Combination Framework for Array Properties. FroCos 2015: 169-185 - [i4]Silvio Ghilardi, Samuel J. van Gool:
A model-theoretic characterization of monadic second order logic on infinite words. CoRR abs/1503.08936 (2015) - 2014
- [j41]Nick Bezhanishvili, Silvio Ghilardi:
The bounded proof property via step algebras and step frames. Ann. Pure Appl. Log. 165(12): 1832-1863 (2014) - [j40]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): 63-109 (2014) - [j39]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): 585-596 (2014) - [j38]Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise:
Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1): 5:1-5:34 (2014) - [c40]Nick Bezhanishvili, Silvio Ghilardi:
Multiple-conclusion Rules, Hypersequents Syntax and Step Frames. Advances in Modal Logic 2014: 54-73 - [c39]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
Booster: An Acceleration-Based Verification Framework for Array Programs. ATVA 2014: 18-23 - [c38]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
A Framework for the Verification of Parameterized Infinite-State Systems. CILC 2014: 303-308 - [c37]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
Decision Procedures for Flat Array Properties. SMT 2014: 51 - [c36]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
Decision Procedures for Flat Array Properties. TACAS 2014: 15-30 - [c35]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
Monotonic Abstraction Techniques: from Parametric to Software Model Checking. MOD* 2014: 1-11 - [p2]Willem Conradie, Silvio Ghilardi, Alessandra Palmigiano:
Unified Correspondence. Johan van Benthem on Logic and Information Dynamics 2014: 933-975 - 2013
- [j37]Alessandro Carioni, Silvio Ghilardi, Silvio Ranise:
Automated Termination in Model-Checking Modulo Theories. Int. J. Found. Comput. Sci. 24(2): 211-232 (2013) - [c34]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
Definability of Accelerated Relations in a Theory of Arrays and Its Applications. FroCos 2013: 23-39 - [c33]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
Acceleration-based safety decision procedure for programs with arrays. LPAR (short papers) 2013: 1-8 - [c32]Nick Bezhanishvili, Silvio Ghilardi:
Bounded Proofs and Step Frames. TABLEAUX 2013: 44-58 - [c31]Silvio Ghilardi:
From free algebras to proof bounds. TACL 2013: 5 - [i3]Francesco Alberti, Silvio Ghilardi, Natasha Sharygina:
Abstraction and Acceleration in SMT-based Model-Checking for Array Programs. CoRR abs/1304.4499 (2013) - 2012
- [j36]Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise:
Quantifier-Free Interpolation of a Theory of Arrays. Log. Methods Comput. Sci. 8(2) (2012) - [j35]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): 29-61 (2012) - [j34]Franz Baader, Silvio Ghilardi, Carsten Lutz:
LTL over description logic axioms. ACM Trans. Comput. Log. 13(3): 21:1-21:32 (2012) - [c30]Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina:
Reachability Modulo Theory Library. SMT@IJCAR 2012: 67-76 - [c29]Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise:
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. IJCAR 2012: 118-133 - [c28]Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina:
SAFARI: SMT-Based Abstraction for Arrays with Interpolants. CAV 2012: 679-685 - [c27]Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina:
Lazy Abstraction with Interpolants for Arrays. LPAR 2012: 46-61 - [c26]Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise:
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. NASA Formal Methods 2012: 279-294 - [e2]Thomas Bolander, Torben Braüner, Silvio Ghilardi, Lawrence S. Moss:
Advances in Modal Logic 9, papers from the ninth conference on "Advances in Modal Logic," held in Copenhagen, Denmark, 22-25 August 2012. College Publications 2012, ISBN 978-1-84890-068-4 [contents] - [i2]Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise:
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. CoRR abs/1203.3730 (2012) - 2011
- [j33]Franz Baader, Silvio Ghilardi:
Unification in modal and description logics. Log. J. IGPL 19(6): 705-730 (2011) - [j32]Guram Bezhanishvili, Silvio Ghilardi, Mamuka Jibladze:
An Algebraic Approach to Subframe Logics. Modal Case. Notre Dame J. Formal Log. 52(2): 187-202 (2011) - [c25]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: 103-118 - [c24]Alessandro Carioni, Silvio Ghilardi, Silvio Ranise:
Automated Termination in Model Checking Modulo Theories. RP 2011: 110-124 - [c23]Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise:
Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. RTA 2011: 171-186 - 2010
- [j31]Silvio Ghilardi, Silvio Ranise:
Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis. Log. Methods Comput. Sci. 6(4) (2010) - [j30]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) - [j29]Silvio Ghilardi:
Continuity, freeness, and filtrations. J. Appl. Non Class. Logics 20(3): 193-217 (2010) - [j28]Silvio Ghilardi, Viorica Sofronie-Stokkermans, Ulrike Sattler, Ashish Tiwari:
Special issue on automated deduction: Decidability, complexity, tractability. J. Symb. Comput. 45(2): 151-152 (2010) - [j27]Silvio Ghilardi:
Book Reviews. Stud Logica 95(3): 443-448 (2010) - [c22]Silvio Ghilardi, Silvio Ranise:
MCMT: A Model Checker Modulo Theories. IJCAR 2010: 22-29 - [c21]Alessandro Carioni, Silvio Ghilardi, Silvio Ranise:
MCMT in the Land of Parametrized Timed Automata. VERIFY@IJCAR 2010: 47-64 - [c20]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: 392-394
2000 – 2009
- 2009
- [c19]Silvio Ghilardi:
Model-Checking of Array-Based Systems: from Foundations to Implementation. FTP 2009 - [c18]Silvio Ghilardi, Silvio Ranise:
Goal-Directed Invariant Synthesis for Model Checking Modulo Theories. TABLEAUX 2009: 173-188 - [e1]Silvio Ghilardi, Roberto Sebastiani:
Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings. Lecture Notes in Computer Science 5749, Springer 2009, ISBN 978-3-642-04221-8 [contents] - 2008
- [j26]Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli:
A comprehensive combination framework. ACM Trans. Comput. Log. 9(2): 8:1-8:54 (2008) - [c17]Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli:
Towards SMT Model Checking of Array-Based Systems. IJCAR 2008: 67-82 - [c16]Franz Baader, Silvio Ghilardi, Carsten Lutz:
LTL over Description Logic Axioms. Description Logics 2008 - [c15]Franz Baader, Silvio Ghilardi, Carsten Lutz:
LTL over Description Logic Axioms. KR 2008: 684-694 - [c14]Silvio Ghilardi, Silvio Ranise, Thomas Valsecchi:
Light-Weight SMT-based Model Checking. AVoCS 2008: 85-102 - 2007
- [j25]Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli:
Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell. 50(3-4): 231-254 (2007) - [j24]Guram Bezhanishvili, Silvio Ghilardi:
An algebraic approach to subframe logics. Intuitionistic case. Ann. Pure Appl. Log. 147(1-2): 84-100 (2007) - [j23]Franz Baader, Silvio Ghilardi:
Connecting many-sorted theories. J. Symb. Log. 72(2): 535-583 (2007) - [c13]Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli:
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. CADE 2007: 362-378 - [c12]Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli:
Noetherianity and Combination Problems. FroCoS 2007: 206-220 - [p1]Torben Braüner, Silvio Ghilardi:
First-order modal logic. Handbook of Modal Logic 2007: 549-620 - [i1]