Alberto Griggio

ORCID

Publication Activity (10 Years)

Years Active: 2006-2024
Publications (10 Years): 63

Top Venues

CoRR

CAV (1)

Formal Methods Syst. Des.

ATVA

University of Trento, Italy (PHD)

Education History

University of Trento, Italy

PHD

Publications

Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, Federico Bonafini, Matteo Campidelli, Andrea Zasa
Reconstructing the High-Level Structure of Legacy Code via Software Model Checking: An Experience Report. FMICS (2024)
Lukas König, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Küperkoch, Dennis Fassbender, Michael Hanselmann
Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development. TACAS (2) (2024)
Yechuan Xia, Alessandro Cimatti, Alberto Griggio, Jianwen Li
Avoiding the Shoals - A New Approach to Liveness Checking. CAV (1) (2024)
Gianluca Redondi, Alessandro Cimatti, Alberto Griggio, Kenneth McMillan
Invariant Checking for SMT-based Systems with Quantifiers. CoRR (2024)
Alessandro Cimatti, Alberto Griggio, Gianluca Redondi
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking. CoRR (2024)
Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li, Geguang Pu
Searching for i-Good Lemmas to Accelerate Safety Model Checking. CAV (2) (2023)
Alberto Griggio, Martin Jonás
Kratos2: An SMT-Based Model Checker for Imperative Programs. CAV (3) (2023)
Srajan Goyal, Alberto Griggio, Jacob Kimblad, Stefano Tonetta
Automatic Generation of Scenarios for System-level Simulation-based Verification of Autonomous Driving Systems. CoRR (2023)
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. TACAS (2) (2023)
Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Angelo Susi
A Formal IDE for Railways: Research Challenges. SEFM Workshops (2022)
Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani
Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test. ATVA (2022)
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Marco Roveri, Stefano Tonetta
Verification modulo theories. Formal Methods Syst. Des. 60 (3) (2022)
Alberto Bombardelli, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Massimo Nazaria, Edoardo Nicolodi, Stefano Tonetta
COMPASTA: Extending TASTE with Formal Design and Verification Functionality. IMBSA (2022)
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jonás
Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation. TACAS (2) (2022)
Alessandro Cimatti, Sara Corfini, Luca Cristoforetti, Marco Di Natale, Alberto Griggio, Stefano Puri, Stefano Tonetta
A comprehensive framework for the analysis of automotive systems. MoDELS (2022)
Alessandro Cimatti, Alberto Griggio, Stefano Tonetta
The VMT-LIB Language and Tools. SMT (2022)
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. Log. Methods Comput. Sci. 18 (3) (2022)
Alessandro Cimatti, Alberto Griggio, Gianluca Redondi
Verification of SMT Systems with Quantifiers. ATVA (2022)
Alessandro Cimatti, Alberto Griggio, Enrico Magnago
LTL falsification in infinite-state systems. Inf. Comput. 289 (Part) (2022)
Erika Ábrahám, James H. Davenport, Matthew England, Alberto Griggio
New Perspectives in Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 22072). Dagstuhl Reports 12 (2) (2022)
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jonás, Greg Kimberly
Analysis of Cyclic Fault Propagation via ASP. LPNMR (2022)
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. CoRR (2021)
Alessandro Cimatti, Alberto Griggio, Gianluca Redondi
Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning. CADE (2021)
Sergio Mover, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Stefano Tonetta
Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. CAV (1) (2021)
Alessandro Cimatti, Alberto Griggio, Enrico Magnago
Proving the Existence of Fair Paths in Infinite-State Systems. VMCAI (2021)
Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonás, Greg Kimberly
Efficient SMT-Based Analysis of Failure Propagation. CAV (2) (2021)
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. TACAS (1) (2021)
Alessandro Cimatti, Alberto Griggio, Enrico Magnago
Automatic Discovery of Fair Paths in Infinite-State Transition Systems. ATVA (2021)
Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonás, Marco Roveri, Roberto Sebastiani, Patrick Trentin
Optimization Modulo Non-linear Arithmetic via Incremental Linearization. FroCoS (2021)
Alberto Griggio, Marco Roveri, Stefano Tonetta
Certifying proofs for SAT-based model checking. Formal Methods Syst. Des. 57 (2) (2021)
Alessandro Cimatti, Alberto Griggio, Stefano Tonetta
The VMT-LIB Language and Tools. CoRR (2021)
James H. Davenport, Matthew England, Alberto Griggio, Thomas Sturm, Cesare Tinelli
Symbolic computation and satisfiability checking. J. Symb. Comput. 100 (2020)
Alessandro Cimatti, Luca Geatti, Alberto Griggio, Greg Kimberly, Stefano Tonetta
Safe Decomposition of Startup Requirements: Verification and Synthesis. TACAS (1) (2020)
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. ISoLA (3) (2020)
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. 272 (2020)
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, Enea Zaffanella
ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics. ARCH@CPSIoTWeek (2019)
Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, Stefano Tonetta
Extending nuXmv with Timed Transition Systems and Timed Temporal Properties. CAV (1) (2019)
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani
Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization. SC-square@SIAM AG (2019)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. CoRR (2018)
Alberto Griggio, Marco Roveri, Stefano Tonetta
Certifying Proofs for LTL Model Checking. FMCAD (2018)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. SAT (2018)
Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, Abhik Roychoudhury
Symbolic execution with existential second-order constraints. ESEC/SIGSOFT FSE (2018)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. ACM Trans. Comput. Log. 19 (3) (2018)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Satisfiability Modulo Transcendental Functions via Incremental Linearization. CoRR (2018)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. SYNASC (2018)
Martin Brain, James H. Davenport, Alberto Griggio
Benchmarking Solvers, SAT-style. SC²@ISSAC (2017)
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler
SC-square: when Satisfiability Checking and Symbolic Computation join forces. ARCADE@CADE (2017)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. TACAS (1) (2017)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Satisfiability Modulo Transcendental Functions via Incremental Linearization. CADE (2017)
Alberto Griggio, Philipp Rümmer
Preface to special issue on satisfiability modulo theories. Formal Methods Syst. Des. 51 (3) (2017)
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods Syst. Des. 49 (3) (2016)
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
Satisfiability Checking meets Symbolic Computation (Project Paper). CoRR (2016)
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
Satisfiability Checking and Symbolic Computation. CoRR (2016)
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
Satisfiability checking and symbolic computation. ACM Commun. Comput. Algebra 50 (4) (2016)
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani
Verilog2SMV: A tool for word-level verification. DATE (2016)
Alberto Griggio, Marco Roveri
Comparing Different Variants of the ic3 Algorithm for Hardware Model Checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 35 (6) (2016)
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
: Satisfiability Checking Meets Symbolic Computation - (Project Paper). CICM (2016)
Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli, Gianni Zampedri
The xSAP Safety Analysis Platform. TACAS (2016)
Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, Sergio Mover
Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations. CAV (1) (2016)
Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli, Gianni Zampedri
The xSAP Safety Analysis Platform. CoRR (2015)
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
HyComp: An SMT-Based Model Checker for Hybrid Systems. TACAS (2015)
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
Parameter Synthesis with IC3 (Informal Presentation). SynCoP (2015)
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Cristian Mattarei
Efficient Anytime Techniques for Model-Based Safety Analysis. CAV (1) (2015)
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta
The nuXmv Symbolic Model Checker. CAV (2014)
Martin Brain, Vijay Victor D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening
Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods Syst. Des. 45 (2) (2014)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. CoRR (2014)
Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario, Alberto Griggio
Towards Pareto-optimal parameter synthesis for monotonic cost functions. FMCAD (2014)
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
IC3 Modulo Theories via Implicit Predicate Abstraction. TACAS (2014)
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
Verifying LTL Properties of Hybrid Systems with K-Liveness. CAV (2014)
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
IC3 Modulo Theories via Implicit Predicate Abstraction. CoRR (2013)
Martin Brain, Vijay Victor D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening
Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. SAS (2013)
Martin Brain, Vijay Victor D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening
An Abstract Interpretation of DPLL(T). VMCAI (2013)
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
The MathSAT5 SMT Solver. TACAS (2013)
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
Parameter synthesis with IC3. FMCAD (2013)
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
A Modular Approach to MaxSAT Modulo Theories. SAT (2013)
Roberto Bruttomesso, Alberto Griggio
Broadening the Scope of SMT-COMP: the Application Track. COMPARE (2012)
Alessandro Cimatti, Alberto Griggio
Software Model Checking via IC3. CAV (2012)
Raian Ali, Alberto Griggio, Anders Franzén, Fabiano Dalpiaz, Paolo Giorgini
Optimizing Monitoring Requirements in Self-adaptive Systems. BMMDS/EMMSAD (2012)
Leopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening
Deciding floating-point logic with systematic abstraction. FMCAD (2012)
David R. Cok, Alberto Griggio, Roberto Bruttomesso, Morgan Deters
The 2012 SMT Competition. SMT@IJCAR (2012)
Alberto Griggio
A Practical Approach to Satisability Modulo Linear Integer Arithmetic. J. Satisf. Boolean Model. Comput. 8 (1/2) (2012)
Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. TACAS (2011)
Alberto Griggio
Effective word-level interpolation for software verification. FMCAD (2011)
Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, Silvia Tomasi
Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT. FroCoS (2011)
Alessandro Cimatti, Alberto Griggio, Andrea Micheli, Iman Narasamdya, Marco Roveri
Kratos - A Software Model Checker for SystemC. CAV (2011)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. J. Artif. Intell. Res. 40 (2011)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Efficient generation of craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12 (1) (2010)
Alessandro Cimatti, Anders Franzén, Alberto Griggio, Krishnamani Kalyanasundaram, Marco Roveri
Tighter integration of BDDs and SMT for Predicate Abstraction. DATE (2010)
Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic Log. Methods Comput. Sci. 8 (3) (2010)
Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani, Cristian Stenico
Satisfiability Modulo the Theory of Costs: Foundations and Applications. TACAS (2010)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Interpolant Generation for UTVPI. CADE (2009)
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani
Software Model Checking via Large-Block Encoding CoRR (2009)
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani
Software model checking via large-block encoding. FMCAD (2009)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories CoRR (2009)
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Ann. Math. Artif. Intell. 55 (1-2) (2009)
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
The MathSAT 4SMT Solver. CAV (2008)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Efficient Interpolant Generation in Satisfiability Modulo Theories. TACAS (2008)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. SAT (2007)
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani
A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. CAV (2007)
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. LPAR (2006)

Alberto Griggio.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Alberto Griggio