You are here

Alberto Griggio

Researcher
  • Phone: 0461314437
  • FBK Povo
Publications

2013

  1. 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
  2. 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
  3. 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
  4. 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
  5. 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
  6. Cimatti A.; Griggio A.; Mover S.; Tonetta S.,
    Parameter Synthesis with IC3,
    Formal Methods in Computer-Aided Design,
    2013
    , (Formal Methods in Compuiter-Aided Desisgn 2013,
    Portland, OR, USA,
    October 20-23, 2013)

2012

  1. Alberto Griggio,
    A Practical Approach to Satisability Modulo Linear Integer Arithmetic,
    in «JOURNAL ON SATISFIABILITY, BOOLEAN MODELING AND COMPUTATION»,
    vol. 8,
    2012
  2. 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
  3. Alessandro Cimatti; Alberto Griggio,
    Software Model Checking via IC3,
    Proceedings of Computer Aided Verification - 24th International Conference, CAV 2012,
    Springer,
    vol.7358,
    2012
    , (Computer Aided Verification - 24th International Conference, CAV 2012,
    Berkeley, CA, USA,
    da 07/07/2012 a 13/07/2012)
  4. 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
    , (Enterprise, Business-Process and Information Systems Modeling - 13th International Conference, BPMDS 2012, 17th International Conference, EMMSAD 2012, and 5th EuroSymposium,
    Gdask, Poland,
    25-26 Giugno 2012)
  5. 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
    , (1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems,
    Manchester, UK,
    30/06/2012)

2011

  1. 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
  2. Alberto Griggio; Thi Thieu Hoa Le; Roberto Sebastiani,
    Proceedings 17th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems,
    vol.To appear,
    2011
    , (TACAS 2011,
    Saarbrücken, Germany,
    26/03/2011-03/04/2011)
  3. Alessandro Cimatti; Alberto Griggio; Andrea Micheli; Iman Narasamdya; Marco Roveri,
    2011
    , (Accepted at CAV 2011 - 23rd International Conference onComputer Aided Verification,
    Cliff Lodge, Snowbird, Utah,
    14-20/07/2011)
  4. 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
    , (Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011,
    Saarbrucken, Germany,
    da 05/10/2011 a 07/10/2011)
  5. 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
    , (International Conference on Formal Methods in Computer-Aided Design, FMCAD '11,
    Austin, TX, USA,
    da 30/10/2011 a 02/11/2011)

2010

  1. 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
  2. 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
    , (DATE 2010,
    Dresden, Germany,
    08-12/03/2010)
  3. 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,
    Berlin / Heidelberg,
    Springer,
    vol.6015,
    2010
    , pp. 99-
    113
    , (TACAS 2010,
    Paphos, Cyprus,
    20-28/03/2010)
  4. Marco Roveri; Alessandro Cimatti; Iman Narasamdya; Andrea Micheli; Daniele Campana; Alberto Griggio; Andrei Tchaltsev,
    2010,

2009

  1. 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»,
    vol. 55,
    n. 1-2,
    2009
    , pp. 66 -
    99
  2. 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
    , (CADE-22,
    McGill University, Montreal, Canada,
    2-7/08/2009)
  3. 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
    , (FMCAD`2009,
    AUSTIN, TX, USA,
    15/11/2009 - 18/11/2009)
  4. Dirk Beyer; Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani,
    Software Model Checking via Large-Block Encoding,
    2009
  5. Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani,
    The problem of computing Craig Interpolants has recently received a lot of interest. In this paper, we address the problem of efficient generation of interpolants for some important fragments of first order logic, which are amenable for effective decision procedures, called Satisfiability Modulo Theory solvers. We make the following contributions. First, we provide interpolation procedures for several basic theories of interest: the theories of linear arithmetic over the rationals, difference logic over rationals and integers, and UTVPI over rationals and integers. Second, we define a novel approach to interpolate combinations of theories, that applies to the Delayed Theory Combination approach. Efficiency is ensured by the fact that the proposed interpolation algorithms extend state of the art algorithms for Satisfiability Modulo Theories. Our experimental evaluation shows that the MathSAT SMT solver can produce interpolants with minor overhead in search, and much more efficiently than other competitor solvers.,
    2009
  6. Dirk Beyer; Alessandro Cimatti; Alberto Griggio; Erkan Keremoglu; Roberto Sebastiani,
    The construction and analysis of an abstract reachability tree (ART) are the basis for a successful method for software verification. The ART represents unwindings of the control-flow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach single-block encoding (SBE). SBE may result in a huge number of program paths to be explored, which constitutes a fundamental source of inefficiency. We propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; we call this approach large-block encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially. Within this framework, we also investigate symbolic representations: for representing abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; for computing abstract-successor states, in addition to Cartesian predicate abstraction as used in SBE, we investigate the use of Boolean predicate abstraction. The new encoding leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors. Our experiments on benchmark C programs show that the large-block encoding outperforms the single-block encoding.,
    2009

2008

  1. 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
    , (CAV 2008,
    Princeton, NJ, USA,
    7-14/07/2008)
  2. 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
    , (TACAS 2008-Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008,
    Budapest, Hungary,
    29/03-06/04/2008)

2007

  1. 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
    , (CAV'07,
    Berlin, Germany,
    2007)
  2. 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
    , (SAT’07,
    Lisbon, Portugal,
    28-31/05/2007)
  3. Roberto Bruttomesso; Alessandro Cimatti; Roberto Sebasatiani; Alberto Griggio; Anders Franzen,
    2007,

2006

  1. 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
    , (LPAR'06,
    Phnom Penh, Cambodia,
    13-17/11/2006)
  2. Roberto Bruttomesso; Alessandro Cimatti; Anders Franzen; Alberto Griggio; Roberto Sebastiani,
    Springer Verlag,
    vol.4246,
    2006
    , pp. 527-
    541
    , (LPAR'06,
    Phnom Penh, Cambodia,
    13-17/11/2006)