Alberto Griggio

Researcher

    Publications

    1. 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
    2. 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, Proceedi...,
      Springer,
      vol. 12078,
      2020
      , pp. 155-
      172
    3. 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
    4. 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
    5. 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
    6. 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
    7. 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
    8. Griggio, Alberto; Roveri, Marco; Tonetta, Stefano,
      Certifying Proofs for LTL Model Checking,
      Formal Methods in Computer-Aided Design, FMCAD 2018,
      2018
      , pp. 225-
      233
    9. 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
    10. 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
    11. Griggio, Alberto; Rümmer, Philipp,
      Preface to special issue on satisfiability modulo theories,
      Formal Methods in System Design,
      vol. 51,
      2017
      , pp. 431-
      432
    12. Bittner, Benjamin; Bozzano, Marco; Cavada, Roberto; Cimatti, Alessandro; Gario, Marco; 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
    13. Á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
    14. Daniel, Jakub; 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
    15. 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
    16. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      Infinite-state invariant checking with IC3 and predicate abstraction,
      in «FORMAL METHODS IN SYSTEM DESIGN»,
      2016
    17. Á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
    18. Cimatti A.; Griggio A.; Mover S.; Tonetta S.,
      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
    19. 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
    20. 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
    21. A. Cimatti;A. Griggio;S. Mover;S. Tonetta,
      IC3 Modulo Theories via Implicit Predicate Abstraction,
      TACAS,
      Springer,
      vol. 8413,
      2014
      , pp. 46-
      61
    22. A. Cimatti;A. Griggio;S. Mover;S. Tonetta,
      Verifying LTL Properties of Hybrid Systems with K-Liveness,
      CAV,
      2014
      , pp. 424-
      440
    23. R. Cavada;A. Cimatti;M. Dorigatti;A. Griggio;A. Mariotti;A. Micheli;S. Mover;M. Roveri;S. Tonetta,
      The nuXmv Symbolic Model Checker,
      CAV,
      2014
      , pp. 334-
      342
    24. 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
    25. Alessandro Cimatti;Alberto Griggio;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
    26. Alessandro Cimatti;Alberto Griggio;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
    27. Cimatti A.; Griggio A.; Mover S.; Tonetta S.,
      Parameter Synthesis with IC3,
      Formal Methods in Computer-Aided Design,
      2013
    28. Martin Brain;Vijay D’Silva;Leopold Haller;Alberto Griggio;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
    29. Martin Brain;Vijay D’Silva;Alberto Griggio;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
    30. Martin Brain;Vijay D’Silva;Alberto Griggio;Leopold Haller;Daniel Kroening,
      Deciding floating-point logic with abstract conflict driven clause learning,
      in «FORMAL METHODS IN SYSTEM DESIGN»,
      2013
    31. Alessandro Cimatti; Alberto Griggio,
      Software Model Checking via IC3,
      Proceedings of Computer Aided Verification - 24th International Conference, CAV 2012,
      Springer,
      vol. 7358,
      2012
    32. Raian Ali; Alberto Griggio; 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
    33. Leopold, Haller; Griggio, Alberto; Martin, Brain; Daniel, Kroening,
      Deciding Floating-Point Logic with Systematic Abstraction,
      Proceedings of FMCAD 2012,
      2012
    34. Roberto Bruttomesso; Alberto Griggio,
      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
    35. Alberto Griggio,
      A Practical Approach to Satisability Modulo Linear Integer Arithmetic,
      in «JOURNAL ON SATISFIABILITY, BOOLEAN MODELING AND COMPUTATION»,
      vol. 8,
      2012
    36. Alberto Griggio; 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
    37. Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani,
      Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories,
      in «THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH»,
      vol. 40,
      2011
      , pp. 701-
      728
    38. Alessandro Cimatti; Alberto Griggio; Andrea Micheli; Iman Narasamdya; Marco Roveri,
      Kratos - A Software Model Checker for SystemC,
      2011
    39. Alberto Griggio; Thi Thieu Hoa Le; Roberto Sebastiani,
      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
    40. Alberto Griggio; 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
    41. Alberto Griggio,
      Effective word-level interpolation for software verification,
      Proceedings of International Conference on Formal Methods in Computer-Aided Design, FMCAD '11,
      FMCAD Inc.,
      2011
    42. Alessandro Cimatti; Anders Franzen; Alberto Griggio; Kalyanasundaram Krishnamani; Marco Roveri,
      Tighter Integration of BDD and SMT for Predicate Abstraction,
      Proceedings of the Design, Automation & Test in Europe,
      2010
      , pp. 1707-
      1712
    43. Alessandro Cimatti; Anders Franzén; Alberto Griggio; Roberto Sebastiani; 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
    44. Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani,
      Efficient generation of craig interpolants in satisfiability modulo theories,
      in «ACM TRANSACTIONS ON COMPUTATIONAL LOGIC»,
      vol. 12,
      n. 1, article 7,
      2010
    45. Marco Roveri; Alessandro Cimatti; Iman Narasamdya; Andrea Micheli; Daniele Campana; Alberto Griggio; Andrei Tchaltsev,
      KRATOS,
      2010
    46. 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
    47. Roberto Bruttomesso; Alessandro Cimatti; Anders Franzen; Alberto Griggio; Roberto Sebastiani,
      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
    48. 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
    49. Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani,
      Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories,
      2009
    50. Dirk Beyer; Alessandro Cimatti; Alberto Griggio; Erkan Keremoglu; Roberto Sebastiani,
      Software Model Checking via Large-Block Encoding,
      2009
    51. Roberto Bruttomesso; Alessandro Cimatti; Anders Franzen; Alberto Griggio; Roberto Sebastiani,
      The MathSAT 4SMT Solver,
      Proceedings of the 20th Int. Conference on Computer Aided Verification,
      Springer-Verlag,
      vol. 5123,
      2008
      , pp. 299-
      303
    52. 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
    53. Roberto Bruttomesso; Alessandro Cimatti; Anders Franzen; Alberto Griggio; Ziyad Hanna; Alexander Nadel; Amit Palti; Roberto Sebastiani,
      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
    54. Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani,
      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
    55. Roberto Bruttomesso; Alessandro Cimatti; Roberto Sebasatiani; Alberto Griggio; Anders Franzen,
      MathSAT,
      2007
    56. Roberto Bruttomesso; Alessandro Cimatti; Anders Franzen; Alberto Griggio; Alessandro Santuari; Roberto Sebastiani,
      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
    57. Roberto Bruttomesso; Alessandro Cimatti; Anders Franzen; Alberto Griggio; Roberto Sebastiani,
      Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis,
      Springer Verlag,
      vol. 4246,
      2006
      , pp. 527-
      541