Alberto Griggio

Researcher

    Publications

    1. Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca,
      Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning,
      28th International Conference on Automated Deduction, Proceedings,
      vol. 12699,
      2021
      , pp. 131-
      147
    2. Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico,
      Proving the Existence of Fair Paths in Infinite-State Systems,
      Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021,
      vol. 12597,
      2021
      , pp. 104-
      126
    3. Bozzano, Marco; Cimatti, Alessandro; Fernandes Pires, Anthony; Griggio, Alberto; Jonas, Martin; Kimberly, Greg,
      Efficient SMT-Based Analysis of Failure Propagation,
      Proceedings of Computer Aided Verification - 33rd International Conference, (CAV2021), Virtual Event, Part II,
      Springer,
      vol. 12760,
      2021
      , pp. 209-
      230
    4. Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano,
      Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems,
      Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, Proceedings, Part I,
      Springer,
      vol. 12759,
      2021
      , pp. 529-
      551
    5. Bigarella, Filippo; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Jonáš, Martin; Roveri, Marco; Sebastiani, Roberto; Trentin, Patrick,
      Optimization Modulo Non-linear Arithmetic via Incremental Linearization,
      Frontiers of Combining Systems 13th International Symposium, FroCoS 2021,
      vol. 12941,
      2021
      , pp. 213-
      231
    6. Griggio, Alberto; Roveri, Marco; Tonetta, Stefano,
      Certifying proofs for SAT-based model checking,
      in «FORMAL METHODS IN SYSTEM DESIGN»,
      vol. 57,
      2021
      , pp. 178-
      210
    7. Mann, Makai; Irfan, Ahmed; Griggio, Alberto; Padon, Oded; Barrett, Clark,
      Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays,
      Tools and Algorithms for the Construction and Analysis of Systems,
      vol. 12651,
      2021
      , pp. 113-
      132
    8. Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico; Roveri, Marco; Tonetta, Stefano,
      SMT-Based Satisfiability of First-Order LTL with Event Freezing Functions and Metric Operators,
      in «INFORMATION AND COMPUTATION»,
      vol. 272,
      2020
    9. Cimatti, Alessandro; Geatti, Luca; Griggio, Alberto; Kimberly, Greg; Tonetta, Stefano,
      Safe Decomposition of Startup Requirements: Verification and Synthesis,
      Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, (TACAS) 2020, Held as Part of theEuropean Joint Conferences on Theory and Practice of Software, (ETAPS) 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part (I),
      Springer,
      vol. 12078,
      2020
      , pp. 155-
      172
    10. 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,
      Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020,
      Springer,
      vol. 12478,
      2020
      , pp. 240-
      254
    11. Davenport, J. H.; England, M.; Griggio, A.; Sturm, T.; Tinelli, C.,
      Symbolic computation and satisfiability checking,
      Journal of Symbolic Computation,
      vol. 100,
      2020
      , pp. 1-
      10
    12. Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico; Roveri, Marco; Tonetta, Stefano,
      Extending nuXmv with Timed Transition Systems and Timed Temporal Properties,
      Proceedings of Computer Aided Verification - 31st International Conference, CAV 2019,
      vol. 11561,
      2019
      , pp. 376-
      386
    13. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto,
      Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization,
      Proceedings of Theory and Applications of Satisfiability Testing – SAT 2018,
      vol. 10929,
      2018
      , pp. 383-
      398
    14. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto,
      Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions,
      in «ACM TRANSACTIONS ON COMPUTATIONAL LOGIC»,
      vol. 19,
      n. 3,
      2018
      , pp. 1-
      52
    15. Mechtaev, Sergey; Griggio, Alberto; Cimatti, Alessandro; Roychoudhury, Abhik,
      Symbolic execution with existential second-order constraints,
      Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018,
      2018
      , pp. 389-
      399
    16. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto,
      Incremental Linearization: A practical approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions,
      Proceedings of 2018 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing,
      2018
    17. Griggio, Alberto; Roveri, Marco; Tonetta, Stefano,
      Certifying Proofs for LTL Model Checking,
      Formal Methods in Computer-Aided Design, FMCAD 2018,
      2018
      , pp. 225-
      233
    18. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto,
      Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF,
      Tools and Algorithms for the Construction and Analysis of Systems,
      vol. 10205,
      2017
      , pp. 58-
      75
    19. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto,
      Satisfiability Modulo Transcendental Functions via Incremental Linearization,
      Automated Deduction – CADE 26,
      vol. 10395,
      2017
      , pp. 95-
      113
    20. Griggio, Alberto; Rümmer, Philipp,
      Preface to special issue on satisfiability modulo theories,
      Formal Methods in System Design,
      vol. 51,
      2017
      , pp. 431-
      432
    21. 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,
      Tools and Algorithms for the Construction and Analysis of Systems,
      Springer Berlin Heidelberg,
      vol. 9636,
      2016
      , pp. 533-
      539
    22. Á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,
      Intelligent Computer Mathematics - 9th International Conference, CICM 2016,
      vol. 9791,
      2016
      , pp. 28-
      43
    23. Jakub, Daniel; Cimatti, Alessandro; Griggio, Alberto; Tonetta, Stefano; Mover, Sergio,
      Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations,
      Computer Aided Verification - 28th International Conference, CAV 2016,
      vol. 9779,
      2016
      , pp. 271-
      291
    24. Irfan, Ahmed; Cimatti, Alessandro; Griggio, Alberto; Roveri, Marco; Sebastiani, Roberto,
      Verilog2SMV: A Tool for Word-level Verification,
      Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016,
      2016
      , pp. 1156-
      1159
    25. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      Infinite-state invariant checking with IC3 and predicate abstraction,
      in «FORMAL METHODS IN SYSTEM DESIGN»,
      2016
    26. Á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,
      in «ACM COMMUNICATIONS IN COMPUTER ALGEBRA»,
      vol. 50,
      n. 4,
      2016
      , pp. 145-
      147
    27. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      HYCOMP - an SMT-based model checker for hybrid systems,
      Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings,
      Springer,
      vol. 9035,
      2015
      , pp. 52-
      67
    28. Bozzano, Marco; Cimatti, Alessandro; Griggio, Alberto; Mattarei, Cristian,
      Efficient Anytime Techniques for Model-Based Safety Analysis,
      Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I,
      vol. 9206,
      2015
      , pp. 603-
      621
    29. Griggio, Alberto; Roveri, Marco,
      Comparing Different Variants of the IC3 Algorithm for Hardware Model Checking,
      in «IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS»,
      2015
      , pp. 1-
      1
    30. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      IC3 Modulo Theories via Implicit Predicate Abstraction,
      TACAS,
      Springer,
      vol. 8413,
      2014
      , pp. 46-
      61
    31. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      Verifying LTL Properties of Hybrid Systems with K-Liveness,
      CAV,
      2014
      , pp. 424-
      440
    32. Cavada, Roberto; Cimatti, Alessandro; Dorigatti, Michele; Griggio, Alberto; Mariotti, Alessandro; Micheli, Andrea; Mover, Sergio; Roveri, Marco; Tonetta, Stefano,
      The nuXmv Symbolic Model Checker,
      CAV,
      2014
      , pp. 334-
      342
    33. Bittner B.; Bozzano M.; Cimatti A.; Gario M.; Griggio A.,
      Towards Pareto-Optimal Parameter Synthesis for Monotonic Cost Functions,
      Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design,
      2014
      , pp. 23-
      30
    34. Cimatti, Alessandro; Griggio, Alberto; Bastiaan Joost, Schaafsma; Roberto, Sebastiani,
      The MathSAT5 SMT Solver,
      in «LECTURE NOTES IN ARTIFICIAL INTELLIGENCE»,
      Lecture Notes in Computer ScienceTools and Algorithms for the Construction and Analysis of Systems,
      vol. 7795,
      2013
      , pp. 93-
      107
    35. Cimatti, Alessandro; Griggio, Alberto; Bastiaan Joost, Schaafsma; Roberto, Sebastiani,
      A Modular Approach to MaxSAT Modulo Theories,
      in «LECTURE NOTES IN ARTIFICIAL INTELLIGENCE»,
      Lecture Notes in Computer ScienceTheory and Applications of Satisfiability Testing – SAT 2013,
      vol. 7962,
      2013
      , pp. 150-
      165
    36. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      Parameter Synthesis with IC3,
      Formal Methods in Computer-Aided Design,
      2013
    37. Martin, Brain; Vijay, D’Silva; Leopold, Haller; Griggio, Alberto; Daniel, Kroening,
      An Abstract Interpretation of DPLL(T)Verification, Model Checking, and Abstract Interpretation,
      in «LECTURE NOTES IN ARTIFICIAL INTELLIGENCE»,
      Lecture Notes in Computer ScienceVerification, Model Checking, and Abstract Interpretation,
      vol. 7737,
      2013
      , pp. 455-
      475
    38. Martin, Brain; Vijay, D’Silva; Griggio, Alberto; Leopold, Haller; Daniel, Kroening,
      Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL,
      in «LECTURE NOTES IN ARTIFICIAL INTELLIGENCE»,
      Lecture Notes in Computer ScienceStatic Analysis,
      vol. 7935,
      2013
      , pp. 412-
      432
    39. Martin, Brain; Vijay, D’Silva; Griggio, Alberto; Leopold, Haller; Daniel, Kroening,
      Deciding floating-point logic with abstract conflict driven clause learning,
      in «FORMAL METHODS IN SYSTEM DESIGN»,
      2013
    40. Cimatti, Alessandro; Griggio, Alberto,
      Software Model Checking via IC3,
      Proceedings of Computer Aided Verification - 24th International Conference, CAV 2012,
      Springer,
      vol. 7358,
      2012
    41. Raian, Ali; Griggio, Alberto; Anders, Franzen; Fabiano, Dalpiaz; Paolo, Giorgini,
      Optimizing Monitoring Requirements in Self-adaptive Systems,
      Proceedings of Enterprise, Business-Process and Information Systems Modeling - 13th International Conference, BPMDS 2012, 17th International Conference, EMMSAD 2012, and 5th EuroSymposium,
      Springer,
      vol. 113,
      2012
    42. Leopold, Haller; Griggio, Alberto; Martin, Brain; Daniel, Kroening,
      Deciding Floating-Point Logic with Systematic Abstraction,
      Proceedings of FMCAD 2012,
      2012
    43. Roberto, Bruttomesso; Griggio, Alberto,
      Broadening the Scope of SMT-COMP: the Application Track,
      Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems,
      vol. 873,
      2012
    44. Griggio, Alberto,
      A Practical Approach to Satisability Modulo Linear Integer Arithmetic,
      in «JOURNAL ON SATISFIABILITY, BOOLEAN MODELING AND COMPUTATION»,
      vol. 8,
      2012
    45. Griggio, Alberto; Thi Thieu Hoa, Le; Roberto, Sebastiani,
      Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic,
      in «LOGICAL METHODS IN COMPUTER SCIENCE»,
      vol. 8,
      n. 3,
      2012
    46. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto,
      Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories,
      in «THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH»,
      vol. 40,
      2011
      , pp. 701-
      728
    47. Cimatti, Alessandro; Griggio, Alberto; Micheli, Andrea; Iman, Narasamdya; Roveri, Marco,
      Kratos - A Software Model Checker for SystemC,
      2011
    48. Griggio, Alberto; Thi Thieu Hoa, Le; Sebastiani, Roberto,
      Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic,
      Proceedings 17th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems,
      vol. To appear,
      2011
    49. Griggio, Alberto; Quoc Sang, Phan; Roberto, Sebastiani; Silvia, Tomasi,
      Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT,
      Proceedings of Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011,
      Springer,
      vol. 6989,
      2011
    50. Griggio, Alberto,
      Effective word-level interpolation for software verification,
      Proceedings of International Conference on Formal Methods in Computer-Aided Design, FMCAD '11,
      FMCAD Inc.,
      2011
    51. Cimatti, Alessandro; Anders, Franzen; Griggio, Alberto; Kalyanasundaram, Krishnamani; Roveri, Marco,
      Tighter Integration of BDD and SMT for Predicate Abstraction,
      Proceedings of the Design, Automation & Test in Europe,
      2010
      , pp. 1707-
      1712
    52. Cimatti, Alessandro; Anders, Franzén; Griggio, Alberto; Sebastiani, Roberto; Cristian, Stenico,
      Satisfiability Modulo the Theory of Costs: Foundations and Applications,
      Proceedings of 16th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems,
      Springer,
      vol. 6015,
      2010
      , pp. 99-
      113
    53. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto,
      Efficient generation of craig interpolants in satisfiability modulo theories,
      in «ACM TRANSACTIONS ON COMPUTATIONAL LOGIC»,
      vol. 12,
      n. 1, article 7,
      2010
    54. Roveri, Marco; Cimatti, Alessandro; Narasamdya, Iman; Micheli, Andrea; Daniele, Campana; Griggio, Alberto; Tchaltsev, Andrei,
      KRATOS,
      2010
    55. Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani,
      Interpolant Generation for UTVPI,
      Proceedings of the 22nd Int. Conference on Automated Deduction,
      Springer Verlag,
      vol. 5663,
      2009
      , pp. 167-
      182
    56. 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,
      in «ANNALS OF MATHEMATICS AND OF ARTIFICIAL INTELLIGENCE»,
      Springer,
      vol. 55,
      n. 1-2,
      2009
      , pp. 66-
      99
    57. Dirk Beyer; Alessandro Cimatti; Alberto Griggio; Erkan Keremoglu; Roberto Sebastiani,
      Software Model Checking via Large-Block Encoding,
      Proceedings of the 9th Conference on Formal Methods in Computer Aided Design,
      2009
    58. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto,
      Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories,
      2009
    59. Dirk, Beyer; Cimatti, Alessandro; Griggio, Alberto; Erkan, Keremoglu; Sebastiani, Roberto,
      Software Model Checking via Large-Block Encoding,
      2009
    60. Bruttomesso, Roberto; Cimatti, Alessandro; Anders, Franzen; Griggio, Alberto; Sebastiani, Roberto,
      The MathSAT 4SMT Solver,
      Proceedings of the 20th Int. Conference on Computer Aided Verification,
      Springer-Verlag,
      vol. 5123,
      2008
      , pp. 299-
      303
    61. Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani,
      Efficient Interpolant Generation in Satisfiability Modulo Theories,
      Proceedings of the 14th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems,
      Springer-Verlag,
      vol. 4963,
      2008
      , pp. 397-
      412
    62. 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,
      Proceedings of the 19th Int. Conference on Computer aided verification,
      Springer-Verlag,
      vol. 4590,
      2007
      , pp. 547-
      560
    63. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto,
      A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories,
      Proceedings of the 10th Int. Conference on Theory and Applications of Satisfiability Testing,
      Springer,
      vol. 4501,
      2007
      , pp. 334-
      339
    64. Roberto, Bruttomesso; Cimatti, Alessandro; Roberto, Sebasatiani; Griggio, Alberto; Anders, Franzen,
      MathSAT,
      2007
    65. 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),
      Proceedings of the 13th Int. Conference on 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning,
      2006
      , pp. 557-
      571
    66. Roberto, Bruttomesso; Cimatti, Alessandro; Anders, Franzen; Griggio, Alberto; Sebastiani, Roberto,
      Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis,
      Springer Verlag,
      vol. 4246,
      2006
      , pp. 527-
      541