Alberto Griggio

Publications

1. Goyal Srajan; Griggio Alberto; Tonetta Stefano, Leveraging Contracts for Failure Monitoring and Identification in Automated Driving Systems
2. Goyal Srajan; Griggio Alberto; Tonetta Stefano, System-level simulation-based verification of Autonomous Driving Systems with the VIVAS framework and CARLA simulator
3. Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Lidström Christian; Redondi Gianluca; Scaglione Giuseppe; Tessi Matteo; Trenti Dylan, Automated Parameterized Verification of a Railway Protection System with Dafny
4. Bozzano Marco; Cimatti Alessandro; Griggio Alberto; Haifani Fajar, Towards a Unifying View of Fault Propagation Analyses and Notations
5. Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Lidström Christian; Redondi Gianluca; Tessi Matteo; Trenti Dylan, Formal Analysis of a Railway Signaling Block Designed in AIDA
6. Sindoni Giulia; Griggio Alberto; Tonetta Stefano, Certifying rlive: A New Proof Strategy for Liveness Model Checking
7. Cimatti Alessandro; Griggio Alberto; Johannsen Christopher; Rozier Kristin Yvonne; Tonetta Stefano, Infinite-State Liveness Checking with rlive
8. Griggio Alberto, Verification Modulo Theories
9. Sindoni Giulia; Pasini Paolo; Cabodi Gianpiero; Camurati Paolo E.; Griggio Alberto; Palena Marco; Roveri Marco; Tonetta Stefano, A Theorem Prover Based Approach for SAT-Based Model Checking Certification
10. Griggio Alberto; Rungta Neha, Editorial: Special issue on formal methods in computer-aided design
11. Bombardelli Alberto; Bonizzi Alberto; Bozzano Marco; Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Nicolodi Edoardo; Tonetta Stefano; Zampedri Gianni, COMPASTA = COMPASS + TASTE
12. Koenig Lukas; Heinzemann Christian; Griggio Alberto; Klauck Michaela; Cimatti Alessandro; Henze Franziska; Tonetta Stefano; Kueperkoch Stefan; Fassbender Dennis; Hanselmann Michael, Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
13. Redondi Gianluca; Cimatti Alessandro; Griggio Alberto; Mcmillan Kenneth, Invariant Checking for SMT-based Systems with Quantifiers
14. Cimatti Alessandro; Griggio Alberto; Redondi Gianluca, Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
15. Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Tonetta Stefano; Bonafini Federico; Campidelli Matteo; Zasa Andrea, Reconstructing the High-Level Structure of Legacy Code via Software Model Checking: An Experience Report
16. Xia Yechuan; Cimatti Alessandro; Griggio Alberto; Li Jianwen, Avoiding the Shoals - A New Approach to Liveness Checking
17. Jonáš Martin; Strejcek Jan; Griggio Alberto, Combining Symbolic Execution with Predicate Abstraction and CEGAR
18. Redondi Gianluca; Cimatti Alessandro; Griggio Alberto, Towards Verification Modulo Theories of asynchronous systems via abstraction refinement
19. Bozzano Marco; Cimatti Alessandro; Cristoforetti Marco; Griggio Alberto; Svaizer Piergiorgio; Tonetta Stefano, Towards Formal Design of FDIR Components with AI
20. Bombardelli Alberto; Cimatti Alessandro; Griggio Alberto; Tonetta Stefano, Another Look at LTL Modulo Theory over Finite and Infinite Traces
21. Cimatti Alessandro; Cristoforetti Luca; Griggio Alberto; Tonetta Stefano; Corfini Sara; Di Natale Marco; Barrau Florian, EVA: a Tool for the Compositional Verification of AUTOSAR Models
22. Xia Yechuan; Becchi Anna; Cimatti Alessandro; Griggio Alberto; Li Jianwen; Pu Geguang, Searching for i-Good Lemmas to Accelerate Safety Model Checking
23. Griggio Alberto; Jonas Martin, Kratos2: an SMT-Based Model Checker for Imperative Programs
24. Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Susi Angelo, A Formal IDE for Railways: Research Challenges
25. Bombardelli Alberto; Bonizzi Alberto; Bozzano Marco; Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Nazaria Massimo; Nicolodi Edoardo; Tonetta Stefano; Zampedri Gianni, COMPASTA: Integrating COMPASS Functionality into TASTE
26. Goyal Srajan; Griggio Alberto; Kimblad Jacob; Tonetta Stefano, Automatic Generation of Scenarios for System-level Simulation-based Verification of Autonomous Driving Systems
27. Bozzano Marco; Cimatti Alessandro; Griggio Alberto; Jonas Martin, Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation
28. Bozzano Marco; Cimatti Alessandro; Griggio Alberto; Jonas Martin; Kimberly Greg, Analysis of Cyclic Fault Propagation via ASP
29. Cimatti Alessandro; Griggio Alberto; Magnago Enrico, LTL falsification in infinite-state systems
30. Bombardelli Alberto; Bozzano Marco; Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Nazaria Massimo; Nicolodi Edoardo; Tonetta Stefano, COMPASTA: Extending TASTE with Formal Design and Verification Functionality
31. Abraham Erika; Davenport James H.; England Matthew; Griggio Alberto, New Perspectives in Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 22072)
32. Cimatti Alessandro; Corfini Sara; Cristoforetti Luca; Di Natale Marco; Griggio Alberto; Puri Stefano; Tonetta Stefano, A comprehensive framework for the analysis of automotive systems
33. Cimatti Alessandro; Griggio Alberto; Redondi Gianluca, Verification of SMT Systems with Quantifiers
34. Cimatti Alessandro; Griggio Alberto; Lipparini Enrico; Sebastiani Roberto, Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test
35. Mann Makai; Irfan Ahmed; Griggio Alberto; Padon Oded; Barrett Clark, Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
36. Cimatti Alessandro; Griggio Alberto; Tonetta Stefano, The VMT-LIB Language and Tools
37. Mann Makai; Irfan Ahmed; Griggio Alberto; Padon Oded; Barrett Clark, Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
38. Cimatti Alessandro; Griggio Alberto; Redondi Gianluca, Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning
39. Griggio Alberto; Roveri Marco; Tonetta Stefano, Certifying proofs for SAT-based model checking
40. Cimatti Alessandro; Griggio Alberto; Magnago Enrico, Proving the Existence of Fair Paths in Infinite-State Systems
41. Bozzano Marco; Cimatti Alessandro; Fernandes Pires Anthony; Griggio Alberto; Jonas Martin; Kimberly Greg, Efficient SMT-Based Analysis of Failure Propagation
42. Mover Sergio; Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Tonetta Stefano, Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems
43. Bigarella Filippo; Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Jonáš Martin; Roveri Marco; Sebastiani Roberto; Trentin Patrick, Optimization Modulo Non-linear Arithmetic via Incremental Linearization
44. Cimatti Alessandro; Griggio Alberto; Magnago Enrico, Automatic Discovery of Fair Paths in Infinite-State Transition Systems
45. Cimatti Alessandro; Griggio Alberto; Magnago Enrico; Roveri Marco; Tonetta Stefano, SMT-Based Satisfiability of First-Order LTL with Event Freezing Functions and Metric Operators
46. Cimatti Alessandro; Geatti Luca; Griggio Alberto; Kimberly Greg; Tonetta Stefano, Safe Decomposition of Startup Requirements: Verification and Synthesis
47. Amendola Arturo; Becchi Anna; Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Scaglione Giuseppe; Susi Angelo; Tacchella Alberto; Tessi Matteo, A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System
48. Davenport J. H.; England M.; Griggio A.; Sturm T.; Tinelli C., Symbolic computation and satisfiability checking
49. Cimatti Alessandro; Griggio Alberto; Magnago Enrico; Roveri Marco; Tonetta Stefano, Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
50. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
51. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
52. Mechtaev Sergey; Griggio Alberto; Cimatti Alessandro; Roychoudhury Abhik, Symbolic execution with existential second-order constraints
53. Griggio Alberto; Roveri Marco; Tonetta Stefano, Certifying Proofs for LTL Model Checking
54. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Incremental Linearization: A practical approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
55. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
56. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Satisfiability Modulo Transcendental Functions via Incremental Linearization
57. Griggio Alberto; Rümmer Philipp, Preface to special issue on satisfiability modulo theories
58. Bittner Benjamin; Bozzano Marco; Cavada Roberto; Cimatti Alessandro; Gario Marco Elio Gustavo; Griggio Alberto; Mattarei Cristian; Micheli Andrea; Zampedri Gianni, The xSAP Safety Analysis Platform
59. Ábrahám Erika; Abbott John; Becker Bernd; Bigatti Anna M.; Brain Martin; Buchberger Bruno; Cimatti Alessandro; Davenport James H.; England Matthew; Fontaine Pascal; Forrest Stephen; Griggio Alberto; Kroening Daniel; Seiler Werner M.; Sturm Thomas, SC^2: Satisfiability Checking Meets Symbolic Computation
60. Jakub Daniel; Cimatti Alessandro; Griggio Alberto; Tonetta Stefano; Mover Sergio, Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
61. Irfan Ahmed; Cimatti Alessandro; Griggio Alberto; Roveri Marco; Sebastiani Roberto, Verilog2SMV: A Tool for Word-level Verification
62. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, Infinite-state invariant checking with IC3 and predicate abstraction
63. Ábrahám E.; Fontaine P.; Forrest S.; Griggio A.; Kroening D.; Seiler W. M.; Sturm T.; Abbott J.; Becker B.; Bigatti A. M.; Brain M.; Buchberger B.; Cimatti A.; Davenport J. H.; England M., Satisfiability checking and symbolic computation
64. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, HYCOMP - an SMT-based model checker for hybrid systems
65. Griggio Alberto; Roveri Marco, Comparing Different Variants of the IC3 Algorithm for Hardware Model Checking
66. Bozzano Marco; Cimatti Alessandro; Griggio Alberto; Mattarei Cristian, Efficient Anytime Techniques for Model-Based Safety Analysis
67. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, IC3 Modulo Theories via Implicit Predicate Abstraction
68. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, Verifying LTL Properties of Hybrid Systems with K-Liveness
69. Cavada Roberto; Cimatti Alessandro; Dorigatti Michele; Griggio Alberto; Mariotti Alessandro; Micheli Andrea; Mover Sergio; Roveri Marco; Tonetta Stefano, The nuXmv Symbolic Model Checker
70. Bittner Benjamin; Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Griggio Alberto, Towards Pareto-Optimal Parameter Synthesis for Monotonic Cost Functions
71. Martin Brain; Vijay D’Silva; Leopold Haller; Griggio Alberto; Daniel Kroening, An Abstract Interpretation of DPLL(T)Verification, Model Checking, and Abstract Interpretation
72. Cimatti Alessandro; Griggio Alberto; Bastiaan Joost Schaafsma; Roberto Sebastiani, The MathSAT5 SMT Solver
73. Cimatti Alessandro; Griggio Alberto; Bastiaan Joost Schaafsma; Roberto Sebastiani, A Modular Approach to MaxSAT Modulo Theories
74. Martin Brain; Vijay D’Silva; Griggio Alberto; Leopold Haller; Daniel Kroening, Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL
75. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, Parameter Synthesis with IC3
76. Martin Brain; Vijay D’Silva; Griggio Alberto; Leopold Haller; Daniel Kroening, Deciding floating-point logic with abstract conflict driven clause learning
77. Cimatti Alessandro; Griggio Alberto, Software Model Checking via IC3
78. Raian Ali; Griggio Alberto; Anders Franzen; Fabiano Dalpiaz; Paolo Giorgini, Optimizing Monitoring Requirements in Self-adaptive Systems
79. Leopold Haller; Griggio Alberto; Martin Brain; Daniel Kroening, Deciding Floating-Point Logic with Systematic Abstraction
80. Roberto Bruttomesso; Griggio Alberto, Broadening the Scope of SMT-COMP: the Application Track
81. Griggio Alberto, A Practical Approach to Satisability Modulo Linear Integer Arithmetic
82. Griggio Alberto; Thi Thieu Hoa Le; Roberto Sebastiani, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
83. Griggio Alberto; Quoc Sang Phan; Roberto Sebastiani; Silvia Tomasi, Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT
84. Griggio Alberto, Effective word-level interpolation for software verification
85. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
86. Griggio Alberto; Thi Thieu Hoa Le; Sebastiani Roberto, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
87. Cimatti Alessandro; Griggio Alberto; Micheli Andrea; Iman Narasamdya; Roveri Marco, Kratos - A Software Model Checker for SystemC
88. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, Efficient generation of craig interpolants in satisfiability modulo theories
89. Roveri Marco; Cimatti Alessandro; Narasamdya Iman; Micheli Andrea; Daniele Campana; Griggio Alberto; Tchaltsev Andrei, KRATOS
90. Cimatti Alessandro; Anders Franzen; Griggio Alberto; Kalyanasundaram Krishnamani; Roveri Marco, Tighter Integration of BDD and SMT for Predicate Abstraction
91. Cimatti Alessandro; Anders Franzén; Griggio Alberto; Sebastiani Roberto; Cristian Stenico, Satisfiability Modulo the Theory of Costs: Foundations and Applications
92. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, Interpolant Generation for UTVPI
93. Bruttomesso Roberto; Cimatti Alessandro; Anders Franzen; Griggio Alberto; Sebastiani Roberto, Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis. Extended version
94. Dirk Beyer; Cimatti Alessandro; Griggio Alberto; Erkan Keremoglu; Sebastiani Roberto, Software Model Checking via Large-Block Encoding
95. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories
96. Dirk Beyer; Cimatti Alessandro; Griggio Alberto; Erkan Keremoglu; Sebastiani Roberto, Software Model Checking via Large-Block Encoding
97. Bruttomesso Roberto; Cimatti Alessandro; Anders Franzen; Griggio Alberto; Sebastiani Roberto, The MathSAT 4SMT Solver
98. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, Efficient Interpolant Generation in Satisfiability Modulo Theories
99. Roberto Bruttomesso; Cimatti Alessandro; Roberto Sebasatiani; Griggio Alberto; Anders Franzen, MathSAT
100. Bruttomesso Roberto; Cimatti Alessandro; Anders Franzen; Griggio Alberto; Ziyad Hanna; Alexander Nadel; Amit Palti; Sebastiani Roberto, A Lazy and Layered SMT ({BV}) Solver for Hard Industrial Verification Problems
101. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
102. Roberto Bruttomesso; Cimatti Alessandro; Anders Franzen; Griggio Alberto; Alessandro Santuari; Sebastiani Roberto, To Ackermann-ize or not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF U T)
103. Roberto Bruttomesso; Cimatti Alessandro; Anders Franzen; Griggio Alberto; Sebastiani Roberto, Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis