List of Publications

Papers in Journals

Gianluca Redondi, Alessandro Cimatti, Alberto Griggio, Kenneth McMillan. Invariant Checking for SMT-based Systems with Quantifiers. ACM Transactions on Computational Logic (TOCL), Accepted on 24 July 2024. PDF.
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Marco Roveri, Stefano Tonetta. Verification Modulo Theories. In Formal Methods in System Design, 2023. PDF.
Alessandro Cimatti, Alberto Griggio, Enrico Magnago. LTL falsification in infinite-state systems. In Information and Computation, 2022. Preprint PDF.
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett. Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. In Logical Methods in Computer Science, August 31, 2022, Volume 18, Issue 3. PDF.
Alberto Griggio, Marco Roveri, Stefano Tonetta. Certifying Proofs for SAT-based Model Checking. In Formal Methods in System Design, 2021. Published version.
Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, Stefano Tonetta. SMT-based satisfiability of first-order LTL with event freezing functions and metric operators. Inf. Comput., 2019. Preprint.
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. ACM Transactions on Computational Logic (TOCL), Volume 19 Issue 3, September 2018. PDF Preprint. Published version.
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta. Infinite-state invariant checking with IC3 and predicate abstraction. In Formal Methods in System Design, 2016. PDF Preprint. Published version.
Alberto Griggio, Marco Roveri. Comparing Different Variants of the IC3 Algorithm for Hardware Model Checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2015. PDF.
Martin Brain, Vijay D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening. Deciding Floating-Point Logic with Abstract Conflict Driven Clause Learning. Formal Methods in System Design, 2013. PDF.
Alberto Griggio, Thi Thieu Hoa Le, and Roberto Sebastiani. Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. Logical Methods in Computer Science, Volume 8, Issue 3, 2012. PDF.
Alberto Griggio, A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 2012. PDF.
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani. Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. Journal of Artificial Intelligence Research (JAIR), Volume 40, April 2011. PDF.
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani. Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories. ACM Transactions on Computational Logic (TOCL), Volume 12, Issue 1, October 2010. PDF.
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani. Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis. Extended version. Annals of Mathematics and Artificial Intelligence. Ed. Springer. PDF.

Conference Papers

Srajan Goyal, Alberto Griggio, Stefano Tonetta. Leveraging Contracts for Failure Monitoring and Identification in Automated Driving Systems. In proc. SEFM 2024. To appear.
Martin Jonáš, Jan Strejček, Alberto Griggio. Combining Symbolic Execution with Predicate Abstraction and CEGAR. In proc. FMCAD 2024. To appear. PDF.
Gianluca Redondi, Alessandro Cimatti, Alberto Griggio. Towards Verification Modulo Theories of asynchronous systems via abstraction refinement. In proc. FMCAD 2024. To appear. PDF.
Yechuan Xia, Alessandro Cimatti, Alberto Griggio, Jianwen Li. Avoiding the Shoals: a New Approach to Liveness Checking. In proc. CAV 2024. PDF.
Lukas Koenig, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Kueperkoch, Dennis Fassbender and Michael Hanselmann. Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development In proc. TACAS 2024. PDF.
Alberto Griggio, Martin Jonáš. Kratos2: an SMT-Based Model Checker for Imperative Programs In proc. CAV 2023. PDF.
Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li, Geguang Pu. Searching for i-Good Lemmas to Accelerate Safety Model Checking. In proc. CAV 2023. PDF.
Alessandro Cimatti, Luca Cristoforetti, Alberto Griggio, Stefano Tonetta, Sara Corfini, Marco Di Natale, Florian Barrau. EVA: a Tool for the Compositional Verification of AUTOSAR Models. In proc. TACAS 2023. PDF.
Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani. Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test. In proc. ATVA 2022. PDF.
Alessandro Cimatti, Alberto Griggio, Gianluca Redondi. Verification of SMT Systems with Quantifiers. In proc. ATVA 2022. PDF.
Alessandro Cimatti, Sara Corfini, Luca Cristoforetti, Marco Di Natale, Alberto Griggio, Stefano Puri, Stefano Tonetta. A comprehensive framework for the analysis of automotive systems. In proc. MoDELS 2022. PDF.
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jonáš, Greg Kimberly. Analysis of Cyclic Fault Propagation via ASP. In proc. LPNMR 2022. PDF.
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jonás. Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation. In proc. TACAS 2022. PDF.
Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonáš, Marco Roveri, Roberto Sebastiani, Patrick Trentin. Optimization Modulo Non-Linear Arithmetic via Incremental Linearization. In proc. FroCoS 2021. PDF.
Alessandro Cimatti, Alberto Griggio, Enrico Magnago. Automatic discovery of fair paths in infinite-state transition systems. In proc. ATVA 2021. PDF.
Sergio Mover, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Stefano Tonetta. Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. In proc. CAV 2021. PDF.
Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonáš, Greg Kimberly. Efficient SMT-based Analysis of Failure Propagation. In proc. CAV 2021. PDF.
Alessandro Cimatti, Alberto Griggio, Gianluca Redondi. Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning. In proc. CADE 2021. PDF.
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett. Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. In proc. TACAS 2021. PDF.
Alessandro Cimatti, Alberto Griggio, Enrico Magnago. Proving the Existence of Fair Paths in Infinite-State Systems. In proc. VMCAI 2021. PDF.
Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Giuseppe Scaglione, Angelo Susi, Alberto Tacchella, Matteo Tessi. A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System. In proc. ISoLA 2020. PDF.
Alessandro Cimatti, Luca Geatti, Alberto Griggio, Greg Kimberly, Stefano Tonetta. Safe Decomposition of Startup Requirements: Verification and Synthesis. In proc. TACAS 2020. PDF.
Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, Stefano Tonetta. Extending nuXmv with Timed Transition Systems and Timed Temporal Properties. In proc. CAV 2019. PDF.
Alberto Griggio, Marco Roveri, Stefano Tonetta. Certifying Proofs for LTL Model Checking. In proc. FMCAD 2018. PDF.
Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, Abhik Roychoudhury. Symbolic Execution with Existential Second-Order Constraints. In proc. ESEC/FSE 2018. PDF.
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. In proc. SAT 2018. PDF.
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. Satisfiability Modulo Transcendental Functions via Incremental Linearization. In proc. CADE 2017. PDF.
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. In proc. TACAS 2017. PDF.
Erika Abraham, John Abbott, Bernd Becker, Anna Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner Seiler, Thomas Sturm. SC^2: Satisfiability Checking Meets Symbolic Computation - (Project Paper). In proc. CICM 2016. PDF.
Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, Sergio Mover. Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. In proc. CAV 2016. Supplementary Web Page.
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani. Verilog2SMV: A tool for word-level verification. In proc. DATE 2016.
Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli, Gianni Zampedri. The xSAP Safety Analysis Platform. In proc. TACAS 2016.
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Cristian Mattarei. Efficient Anytime Techniques for Model-Based Safety Analysis. In proc. CAV 2015. PDF.
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta. HyCOMP - an SMT-based model checker for hybrid systems. In proc. TACAS 2015. PDF.
Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario, Alberto Griggio. Towards Pareto-Optimal Parameter Synthesis for Monotonic Cost Functions. In proc. FMCAD 2014. PDF.
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta. Verifying LTL properties of hybrid systems with K-liveness. In proc. CAV 2014. PDF.
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta. The nuXmv Symbolic Model Checker. In proc. CAV 2014. PDF.
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta. IC3 Modulo Theories via Implicit Predicate Abstraction. In proc. TACAS 2014. PDF.
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta. Parameter Synthesis with IC3. In proc. FMCAD 2013. PDF.
Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma, Roberto Sebastiani. A Modular Approach to MaxSAT Modulo Theories. In proc. SAT 2013. PDF.
Martin Brain, Vijay D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening. Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. In proc. SAS 2013. PDF.
Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma, Roberto Sebastiani. The MathSAT5 SMT Solver. In proc. TACAS 2013. PDF.
Martin Brain, Vijay D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening. An Abstract Interpretation of DPLL(T). In proc. VMCAI 2013. PDF.
Leopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening. Deciding Floating-Point Logic with Systematic Abstraction. In proc. FMCAD 2012. PDF.
Alessandro Cimatti and Alberto Griggio. Software Model Checking via IC3. In proc. CAV 2012. PDF.
R. Ali, A. Griggio, A. Franzen, A. Dalpiaz, P. Giorgini, Optimizing Monitoring Requirements in Self-Adaptive Systems, In proc. EMMSAD/EuroSymposium 2012, June 2012.
Alberto Griggio. Effective Word-Level Interpolation for Software Verification. In proc. FMCAD 2011. PDF.
Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, and Silvia Tomasi. Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT. In proc. FroCos 2011. PDF.
Alessandro Cimatti, Alberto Griggio, Andrea Micheli, Iman Narasamdya, and Marco Roveri. Kratos - a Software Model Checker for SystemC. In proc. CAV 2011. PDF.
Alberto Griggio, Thi Thieu Hoa Le, and Roberto Sebastiani. Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. In proc. TACAS 2011. PDF.
Alessandro Cimatti, Anders Franzen, Alberto Griggio, Roberto Sebastiani and Cristian Stenico. Satisfiability Modulo the Theory of Costs: Foundations and Applications. In proc. TACAS 2010. PDF.
A. Cimatti, A. Franzen, A. Griggio, K. Kalyanasundaram, M. Roveri. Tighter Integration of BDD and SMT for Predicate Abstraction. In proc. DATE 2010. PDF.
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, Erkan Keremoglu, Roberto Sebastiani. Software Model Checking via Large-Block Encoding. In proc. FMCAD'09, 2009. PDF.
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani. Interpolant Generation for UTVPI. In proc. CADE-22, 2009. PDF.
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani. The MathSAT 4 SMT Solver. In proc. CAV'08, 2008. PDF.
A. Cimatti, A. Griggio, R. Sebastiani. Efficient Interpolant Generation in Satisfiability Modulo Theories. In proc. TACAS'08, 2008.
R. Bruttomesso, A. Cimatti, A. Franzen, A. Griggio, Z. Hanna, A. Nadel, A. Palti, R. Sebastiani. A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems. In proc. CAV'07, 2007. PDF.
A. Cimatti, A. Griggio, R. Sebastiani, A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. In proc. SAT'07, 2007. PDF.
R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, R. Sebastiani, Delayed Theory Combination vs Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis. In proc. LPAR'06, 2006. PDF.
R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, A. Santuari, R. Sebastiani, To Ackermann-ize or not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF U T). In proc. LPAR'06, 2006. PDF.
L. Colussi, G. Filè, A. Griggio, Precise Analysis of pi-calculus in Cubic Time, In proc. TCS2004, 2004. PDF.

PhD Thesis

A. Griggio, An Effective SMT Engine for Formal Verification, DISI, University of Trento, December 2009. PDF.

Workshop Papers

Alessandro Cimatti, Alberto Griggio, Gianluca Redondi. Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking.In Dafny workshop 2024. PDF.
Alessandro Cimatti, Alberto Griggio, Stefano Tonetta. The VMT-LIB Language and Tools.In SMT 2022. PDF.
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization. In proc. SC-Square workshop 2019. PDF.
A. Griggio, M. Roveri, Comparing Different Variants of the IC3 Algorithm for Hardware Model Checking, At DIFTS 2014 Workshop.
R. Bruttomesso, A. Griggio, Broadening the Scope of SMT-COMP: the Application Track, At COMPARE 2012 Workshop, June 2012. PDF.
A. Griggio, A Practical Approach to SMT(LA(Z)), At SMT'10 Workshop, July 2010. PDF.
A. Griggio, R. Sebastiani, S. Tomasi, Stochastic Local Search for SMT: a Preliminary Report, At SMT'09 Workshop, August 2009. PDF.

Technical Reports

A. Cimatti, A. Griggio, R. Sebastiani. Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories, 2009. PDF.
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, Erkan Keremoglu, Roberto Sebastiani. Software Model Checking via Large-Block Encoding. Extended version of FMCAD'09 paper, DISI, 2009. PDF.
A. Cimatti, A. Griggio, R. Sebastiani. Efficient Interpolant Generation in Satisfiability Modulo Theories. Extended version of TACAS'08 paper, DIT, 2008. PDF.
A. Cimatti, A. Griggio, R. Sebastiani, A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. Extended version of SAT'07 paper, DIT, 2007. PDF.
R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, R. Sebastiani, Delayed Theory Combination vs Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis. Extended version of LPAR'06 paper, DIT, 2006. PDF.

Master's Thesis

A. Griggio, Progettazione e realizzazione di una tattica di dimostrazione automatica basata su paramodulazione per il proof-assistant Matita. University of Bologna, October 2005. PDF (In Italian). Short summary (in English): PDF.

Back to Homepage