To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT). - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Alessandro Santuari; Roberto Sebastiani (LPAR, 2006)

A Lazy and Layered SMT($ mathcal{BV}$) Solver for Hard Industrial Verification Problems. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Ziyad Hanna; Alexander Nadel; Amit Palti; Roberto Sebastiani (CAV, 2007)

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (SAT, 2007)

The MathSAT 4SMT Solver. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Roberto Sebastiani (CAV, 2008)

Efficient Interpolant Generation in Satisfiability Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (TACAS, 2008)

Interpolant Generation for UTVPI. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (CADE, 2009)

Software model checking via large-block encoding. - Dirk Beyer 001; Alessandro Cimatti; Alberto Griggio; M. Erkan Keremoglu; Roberto Sebastiani (FMCAD, 2009)

Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Roberto Sebastiani (Ann. Math. Artif. Intell., 2009)

An Effective SMT Engine for Formal Verification. - Alberto Griggio (2009)

Tighter integration of BDDs and SMT for Predicate Abstraction. - Alessandro Cimatti; Anders Franzén; Alberto Griggio; Krishnamani Kalyanasundaram; Marco Roveri (DATE, 2010)

Satisfiability Modulo the Theory of Costs: Foundations and Applications. - Alessandro Cimatti; Anders Franzén; Alberto Griggio; Roberto Sebastiani; Cristian Stenico (TACAS, 2010)

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic - Alberto Griggio; Thi Thieu Hoa Le; Roberto Sebastiani (Log. Methods Comput. Sci., 2010)

Efficient generation of craig interpolants in satisfiability modulo theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (ACM Trans. Comput. Log., 2010)

Kratos - A Software Model Checker for SystemC. - Alessandro Cimatti; Alberto Griggio; Andrea Micheli; Iman Narasamdya; Marco Roveri (CAV, 2011)

Effective word-level interpolation for software verification. - Alberto Griggio (FMCAD, 2011)

Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT. - Alberto Griggio; Quoc-Sang Phan; Roberto Sebastiani; Silvia Tomasi (FroCoS, 2011)

Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (J. Artif. Intell. Res., 2011)

Broadening the Scope of SMT-COMP: the Application Track. - Roberto Bruttomesso; Alberto Griggio (COMPARE, 2012)

The 2012 SMT Competition. - David R. Cok; Alberto Griggio; Roberto Bruttomesso; Morgan Deters (SMT@IJCAR, 2012)

Optimizing Monitoring Requirements in Self-adaptive Systems. - Raian Ali; Alberto Griggio; Anders Franzén; Fabiano Dalpiaz; Paolo Giorgini (BMMDS/EMMSAD, 2012)

Software Model Checking via IC3. - Alessandro Cimatti; Alberto Griggio (CAV, 2012)

Deciding floating-point logic with systematic abstraction. - Leopold Haller; Alberto Griggio; Martin Brain; Daniel Kroening (FMCAD, 2012)

A Practical Approach to Satisability Modulo Linear Integer Arithmetic. - Alberto Griggio (J. Satisf. Boolean Model. Comput., 2012)

Parameter synthesis with IC3. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (FMCAD, 2013)

Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. - Martin Brain; Vijay Victor D'Silva; Alberto Griggio; Leopold Haller; Daniel Kroening (SAS, 2013)

A Modular Approach to MaxSAT Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Bastiaan Joost Schaafsma; Roberto Sebastiani (SAT, 2013)

The MathSAT5 SMT Solver. - Alessandro Cimatti; Alberto Griggio; Bastiaan Joost Schaafsma; Roberto Sebastiani (TACAS, 2013)

An Abstract Interpretation of DPLL(T). - Martin Brain; Vijay Victor D'Silva; Leopold Haller; Alberto Griggio; Daniel Kroening (VMCAI, 2013)

The nuXmv Symbolic Model Checker. - Roberto Cavada; Alessandro Cimatti; Michele Dorigatti; Alberto Griggio; Alessandro Mariotti; Andrea Micheli; Sergio Mover; Marco Roveri; Stefano Tonetta (CAV, 2014)

Verifying LTL Properties of Hybrid Systems with K-Liveness. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (CAV, 2014)

Towards Pareto-optimal parameter synthesis for monotonic cost functions. - Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Marco Gario; Alberto Griggio (FMCAD, 2014)

IC3 Modulo Theories via Implicit Predicate Abstraction. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (TACAS, 2014)

Deciding floating-point logic with abstract conflict driven clause learning. - Martin Brain; Vijay Victor D'Silva; Alberto Griggio; Leopold Haller; Daniel Kroening (Formal Methods Syst. Des., 2014)

Efficient Anytime Techniques for Model-Based Safety Analysis. - Marco Bozzano; Alessandro Cimatti; Alberto Griggio; Cristian Mattarei (CAV (1), 2015)

Parameter Synthesis with IC3 (Informal Presentation). - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (SynCoP, 2015)

HyComp: An SMT-Based Model Checker for Hybrid Systems. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (TACAS, 2015)

Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations. - Jakub Daniel; Alessandro Cimatti; Alberto Griggio; Stefano Tonetta; Sergio Mover (CAV (1), 2016)

Verilog2SMV: A tool for word-level verification. - Ahmed Irfan; Alessandro Cimatti; Alberto Griggio; Marco Roveri; Roberto Sebastiani (DATE, 2016)

SC2: Satisfiability Checking Meets Symbolic Computation - (Project Paper). - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (CICM, 2016)

The xSAP Safety Analysis Platform. - Benjamin Bittner; Marco Bozzano; Roberto Cavada; Alessandro Cimatti; Marco Gario; Alberto Griggio; Cristian Mattarei; Andrea Micheli; Gianni Zampedri (TACAS, 2016)

Satisfiability checking and symbolic computation. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (ACM Commun. Comput. Algebra, 2016)

Satisfiability Checking meets Symbolic Computation (Project Paper). - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (CoRR, 2016)

Infinite-state invariant checking with IC3 and predicate abstraction. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (Formal Methods Syst. Des., 2016)

Comparing Different Variants of the ic3 Algorithm for Hardware Model Checking. - Alberto Griggio; Marco Roveri (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2016)

SC-square: when Satisfiability Checking and Symbolic Computation join forces. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Vijay Ganesh 001; Alberto Griggio; et al. (ARCADE@CADE, 2017)

Satisfiability Modulo Transcendental Functions via Incremental Linearization. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (CADE, 2017)

Benchmarking Solvers, SAT-style. - Martin Brain; James H. Davenport; Alberto Griggio (SC²@ISSAC, 2017)

Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (TACAS (1), 2017)

Preface to special issue on satisfiability modulo theories. - Alberto Griggio; Philipp Rümmer (Formal Methods Syst. Des., 2017)

Certifying Proofs for LTL Model Checking. - Alberto Griggio; Marco Roveri; Stefano Tonetta (FMCAD, 2018)

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (SAT, 2018)

Symbolic execution with existential second-order constraints. - Sergey Mechtaev; Alberto Griggio; Alessandro Cimatti; Abhik Roychoudhury (ESEC/SIGSOFT FSE, 2018)

Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (SYNASC, 2018)

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (ACM Trans. Comput. Log., 2018)

Extending nuXmv with Timed Transition Systems and Timed Temporal Properties. - Alessandro Cimatti; Alberto Griggio; Enrico Magnago; Marco Roveri; Stefano Tonetta (CAV (1), 2019)

ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics. - Goran Frehse; Alessandro Abate; Dieky Adzkiya; Anna Becchi; Lei Bu; Alessandro Cimatti; Mirco Giacobbe; Alberto Griggio; Sergio Mover; Muhammad Syifa'ul Mufid; Idriss Riouak; Stefano Tonetta; et al. (ARCH@CPSIoTWeek, 2019)

Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization. - Ahmed Irfan; Alessandro Cimatti; Alberto Griggio; Marco Roveri; Roberto Sebastiani (SC-square@SIAM AG, 2019)

A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System. - Arturo Amendola; Anna Becchi; Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Giuseppe Scaglione; Angelo Susi; Alberto Tacchella; Matteo Tessi (ISoLA (3), 2020)

Safe Decomposition of Startup Requirements: Verification and Synthesis. - Alessandro Cimatti; Luca Geatti; Alberto Griggio; Greg Kimberly; Stefano Tonetta (TACAS (1), 2020)

SMT-based satisfiability of first-order LTL with event freezing functions and metric operators. - Alessandro Cimatti; Alberto Griggio; Enrico Magnago; Marco Roveri; Stefano Tonetta (Inf. Comput., 2020)

Symbolic computation and satisfiability checking. - James H. Davenport; Matthew England 001; Alberto Griggio; Thomas Sturm 001; Cesare Tinelli (J. Symb. Comput., 2020)

Automatic Discovery of Fair Paths in Infinite-State Transition Systems. - Alessandro Cimatti; Alberto Griggio; Enrico Magnago (ATVA, 2021)

Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning. - Alessandro Cimatti; Alberto Griggio; Gianluca Redondi (CADE, 2021)

Efficient SMT-Based Analysis of Failure Propagation. - Marco Bozzano; Alessandro Cimatti; Anthony Fernandes Pires; Alberto Griggio; Martin Jonás; Greg Kimberly (CAV (2), 2021)

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. - Sergio Mover; Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Stefano Tonetta (CAV (1), 2021)

Optimization Modulo Non-linear Arithmetic via Incremental Linearization. - Filippo Bigarella; Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Martin Jonás; Marco Roveri; Roberto Sebastiani; Patrick Trentin (FroCoS, 2021)

Proving the Existence of Fair Paths in Infinite-State Systems. - Alessandro Cimatti; Alberto Griggio; Enrico Magnago (VMCAI, 2021)

Certifying proofs for SAT-based model checking. - Alberto Griggio; Marco Roveri; Stefano Tonetta (Formal Methods Syst. Des., 2021)

Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test. - Alessandro Cimatti; Alberto Griggio; Enrico Lipparini; Roberto Sebastiani (ATVA, 2022)

Verification of SMT Systems with Quantifiers. - Alessandro Cimatti; Alberto Griggio; Gianluca Redondi (ATVA, 2022)

COMPASTA: Extending TASTE with Formal Design and Verification Functionality. - Alberto Bombardelli; Marco Bozzano; Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Massimo Nazaria; Edoardo Nicolodi; Stefano Tonetta (IMBSA, 2022)

Analysis of Cyclic Fault Propagation via ASP. - Marco Bozzano; Alessandro Cimatti; Alberto Griggio; Martin Jonás; Greg Kimberly (LPNMR, 2022)

A comprehensive framework for the analysis of automotive systems. - Alessandro Cimatti; Sara Corfini; Luca Cristoforetti; Marco Di Natale; Alberto Griggio; Stefano Puri; Stefano Tonetta (MoDELS, 2022)

A Formal IDE for Railways: Research Challenges. - Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Angelo Susi (SEFM Workshops, 2022)

The VMT-LIB Language and Tools. - Alessandro Cimatti; Alberto Griggio; Stefano Tonetta (SMT, 2022)

Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation. - Marco Bozzano; Alessandro Cimatti; Alberto Griggio; Martin Jonás (TACAS (2), 2022)

New Perspectives in Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 22072). - Erika Ábrahám; James H. Davenport; Matthew England 001; Alberto Griggio (Dagstuhl Reports, 2022)

Verification modulo theories. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Marco Roveri; Stefano Tonetta (Formal Methods Syst. Des., 2022)

LTL falsification in infinite-state systems. - Alessandro Cimatti; Alberto Griggio; Enrico Magnago (Inf. Comput., 2022)

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. - Makai Mann; Ahmed Irfan; Alberto Griggio; Oded Padon; Clark W. Barrett (Log. Methods Comput. Sci., 2022)

Kratos2: An SMT-Based Model Checker for Imperative Programs. - Alberto Griggio; Martin Jonás (CAV (3), 2023)

Searching for i-Good Lemmas to Accelerate Safety Model Checking. - Yechuan Xia; Anna Becchi; Alessandro Cimatti; Alberto Griggio; Jianwen Li; Geguang Pu (CAV (2), 2023)

EVA: a Tool for the Compositional Verification of AUTOSAR Models. - Alessandro Cimatti; Luca Cristoforetti; Alberto Griggio; Stefano Tonetta; Sara Corfini; Marco Di Natale; Florian Barrau (TACAS (2), 2023)

Automatic Generation of Scenarios for System-level Simulation-based Verification of Autonomous Driving Systems. - Srajan Goyal; Alberto Griggio; Jacob Kimblad; Stefano Tonetta (FMAS@iFM, 2023)

Artifact for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2023)

Supplementary Material for TACAS Submission "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2023)

Artifact for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2023)

Supplementary Material for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2023)

Another Look at LTL Modulo Theory over Finite and Infinite Traces. - Alberto Bombardelli; Alessandro Cimatti; Alberto Griggio; Stefano Tonetta (Principles of Verification (1), 2024)

Avoiding the Shoals - A New Approach to Liveness Checking. - Yechuan Xia; Alessandro Cimatti; Alberto Griggio; Jianwen Li (CAV (1), 2024)

Combining Symbolic Execution with Predicate Abstraction and CEGAR. - Martin Jonás; Jan Strejcek; Alberto Griggio (FMCAD, 2024)

Towards Verification Modulo Theories of Asynchronous Systems via Abstraction Refinement. - Gianluca Redondi; Alessandro Cimatti; Alberto Griggio (FMCAD, 2024)

Reconstructing the High-Level Structure of Legacy Code via Software Model Checking: An Experience Report. - Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Stefano Tonetta; Federico Bonafini; Matteo Campidelli; Andrea Zasa (FMICS, 2024)

Towards Formal Design of FDIR Components with AI. - Marco Bozzano; Alessandro Cimatti; Marco Cristoforetti; Alberto Griggio; Piergiorgio Svaizer; Stefano Tonetta (ISoLA (4), 2024)

Leveraging Contracts for Failure Monitoring and Identification in Automated Driving Systems. - Srajan Goyal; Alberto Griggio; Stefano Tonetta (SEFM, 2024)

Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development. - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (TACAS (2), 2024)

Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking. - Alessandro Cimatti; Alberto Griggio; Gianluca Redondi (CoRR, 2024)

Invariant Checking for SMT-Based Systems with Quantifiers. - Gianluca Redondi; Alessandro Cimatti; Alberto Griggio; Kenneth L. McMillan (ACM Trans. Comput. Log., 2024)

Supplementary Material for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2024)

Supplementary Material for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2024)

Artifact for CAV'24 paper "Avoiding the Shoals - A New Approach to Liveness Checking". - Yechuan Xia; Alessandro Cimatti; Alberto Griggio; Jianwen Li (Zenodo, 2024)

A Theorem Prover Based Approach for SAT-Based Model Checking Certification. - Giulia Sindoni; Paolo Pasini; Gianpiero Cabodi; Paolo E. Camurati; Alberto Griggio; Marco Palena; Marco Roveri; Stefano Tonetta (CADE, 2025)

Automated Parameterized Verification of a Railway Protection System with Dafny. - Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Christian Lidström; Gianluca Redondi; Giuseppe Scaglione; Matteo Tessi; Dylan Trenti (CAV (4), 2025)

Infinite-State Liveness Checking with rlive. - Alessandro Cimatti; Alberto Griggio; Christopher Johannsen; Kristin Yvonne Rozier; Stefano Tonetta (CAV (1), 2025)

System-level simulation-based verification of Autonomous Driving Systems with the VIVAS framework and CARLA simulator. - Srajan Goyal; Alberto Griggio; Stefano Tonetta (Sci. Comput. Program., 2025)