You are here

Alessandro Cimatti

Head of Unit
  • Phone: 0461314320
  • FBK Povo
Short bio
Research interests
Automated Planning Satisfiability Modulo Theories Verification Modulo Theories Contract-Based Design Symbolic Model Checking Safety Assessment
Publications

2013

  1. Alessandro Cimatti; Sergio Mover; Stefano Tonetta,
    SMT-based scenario verification for hybrid systems,
    in «FORMAL METHODS IN SYSTEM DESIGN»,
    vol. 42,
    n. 1,
    2013
    , pp. 46 -
    66
  2. Alessandro Cimatti;Iman Narasamdya;Marco Roveri,
    Software Model Checking SystemC,
    in «IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS»,
    vol. 32,
    2013
    , pp. 774 -
    787
  3. Marco Bozzano; Alessandro Cimatti; Cristian Mattarei,
    Automated Analysis of Reliability Architectures,
    18th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2013, Singapore, July 17-19, 2013,
    IEEE Computer Society,
    2013
    , pp. 198-
    207
    , (International Conference on Engineering of Complex Computer Systems,
    Singapore,
    07/17/2013 07/19/2013)
  4. Alessandro Cimatti; Andrea Micheli; Marco Roveri,
    AAAI,
    David Leake,
    2013
    , pp. 195-
    201
    , (Twenty-Seventh AAAI Conference on Artificial Intelligence,
    Bellevue, Washington, USA,
    14/07/2013 - 18/07/2013)
  5. 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
  6. 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
  7. Bozzano M.; Cimatti A.; Gario M.; Tonetta S.,
    AAAI Workshops,
    2013
    , (Workshops at the Twenty-Seventh AAAI Conference on Artificial Intelligence,
    Bellevue, Washington, USA,
    14–18 July 2013)
  8. Bozzano M.; Cimatti A.; Gario M.; Tonetta S.,
    Formal Specification and Synthesis of FDI through an Example,
    Proceedings of the 24th International Workshop on Principles of Diagnosis,
    2013
    , (The 24th International Workshop on Principles of Diagnosis,
    Jerusalem, Israel,
    October 1-4, 2013)
  9. Mover S.; Cimatti A.; Tiwari A.; Tonetta S.,
    Time-aware Relational Abstractions for Hybrid Systems,
    Proceedings of the 13th International Conference on Embedded Software,
    2013
    , (International Conference on Embedded Software,
    Montreal, Canada,
    October 2013)
  10. 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)
  11. Marco Bozzano; Alessandro Cimatti; Cristian Mattarei,
    Efficient Analysis of Reliability Architectures via Predicate Abstraction,
    Hardware and Software: Verification and Testing - 9th International Haifa Verification Conference,
    Springer,
    vol.8244,
    2013
    , pp. 279-
    294
    , (Ninth Haifa Verification Conference,
    Haiva, Israel,
    5 - 7 November 2013)
  12. Cimatti A.; Dorigatti M.; Tonetta S.,
    OCRA: A tool for checking the refinement of temporal contracts,
    in «AUTOMATED SOFTWARE ENGINEERING»
    ASE 2013,
    2013
    , pp. 702-
    705

2012

  1. Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta,
    Validation of Requirements for Hybrid Systems: a Formal Approach,
    in «ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY»,
    vol. 21,
    n. 4,
    2012
    , pp. 22:1 -
    22:34
  2. Alessandro Cimatti; Iman Narasamdya; Marco Roveri,
    Software Model Checking with Explicit Scheduler and Symbolic Threads,
    in «LOGICAL METHODS IN COMPUTER SCIENCE»,
    vol. 8,
    2012
    , pp. 1 -
    42
  3. Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Xavier Olive,
    Symbolic Synthesis of Observability Requirements for Diagnosability,
    Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence,
    AAAI Press,
    2012
    , (AAAI 2012: Twenty-Sixth AAAI Conference on Artificial Intelligence,
    Toronto, Canada,
    da 07/22/2012 a 07/26/2012)
  4. 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)
  5. Alessandro Cimatti; Raffaele Corvino; Armando Lazzaro; Iman Narasamdya; Tiziana Rizzo; Marco Roveri; Angela Sanseviero; Andrei Tchaltsev,
    Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System,
    CAV,
    Springer,
    vol.7358,
    2012
    , pp. 378-
    393
    , (Computer Aided Verification - 24th International Conference, CAV 2012,
    Berkeley, CA, USA,
    da 07/07/2012 a 07/13/2012)
  6. Alessandro Cimatti; Iman Narasamdya; Marco Roveri,
    Verification of Parametric System Designs,
    2012
    , (Formal Methods in Computer Aided Design (FMCAD) 2012,
    Cambridge, UK,
    da 10/22/2012 a 10/25/2012)
  7. Alessandro Cimatti; Andrea Micheli; Marco Roveri,
    Solving Temporal Problems using SMT: Weak Controllability,
    Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence,
    AAAI Press,
    2012
    , (AAAI 2012,
    Toronto, Canada,
    da 07/22/2012 a 07/26/2012)
  8. Alessandro Cimatti; Andrea Micheli; Marco Roveri,
    Solving Temporal Problems using SMT: Strong Controllability,
    Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming,
    2012
    , (CP 2012,
    Quebec City, Canada,
    da 10/08/2012 a 10/12/2012)
  9. Alessandro Cimatti; Sergio Mover; Stefano Tonetta,
    SMT-Based Verification of Hybrid Systems,
    2012
    , (Twenty-Sixth AAAI Conference on Artificial Intelligence,
    Toronto, Ontario, Canada,
    July 22-26, 2012)
  10. A. Cimatti; S. Tonetta,
    A Property-Based Proof System for Contract-Based Design,
    2012
    , (38th EUROMICRO Conference on Software Engineering and Advanced Applications, SEAA 2012,
    Cesme, Turkey,
    da 09/05/2012 a 09/07/2012)
  11. A. Cimatti; S. Mover; S. Tonetta,
    Quantifier-free encoding of hybrid systems with non-linear dynamics,
    Proceedings of the 12th Conference on Formal Methods in Computer-Aided Design (FMCAD 2012),
    2012
    , (International Conference on Formal Methods in Computer-Aided Design, FMCAD12,
    Cambridge, UK,
    da 10/22/2012 a 10/25/2012)
  12. Elena Alaña; Héctor Naranjo; Yuri Yushtein; Marco Bozzano; Alessandro Cimatti; Marco Gario; Régis de Ferluc; Gérard Garcia,
    Automated generation of FDIR for the compass integrated toolset (AUTOGEF),
    2012
    , (DASIA 2012,
    Dubrovnik, Croatia,
    14/05/2012 - 16/05/2012)
  13. Robin Steel; Alexander Hoffman; Mark Niézette; Alessandro Cimatti; Marco Roveri; Konstantinos Kapellos; Alessandro Donati; Nicola Policella,
    Innovative Rover Operations Concepts - Autonomous Planner (IRONCAP) - Supporting Rover Operations Planning on Ground,
    SpaceOps 2012 Conference,
    2012
    , (12th International Conference on Space Operations, SpaceOps, At Stockholm, Sweden,
  14. A. Cimatti,
    Formal Methods in Computer-Aided Design, FMCAD 2012,
    IEEE,
    2012
    , pp. 4-
    , (Formal Methods in Computer-Aided Design,
    Cambridge, UK,
    22-25 October 2012)
  15. Alessandro Cimatti; Roberto Sebastiani (eds.),
    Theory and Applications of Satisfiability Testing – SAT 2012,
    Springer,
    2012

2011

  1. Alessandro Cimatti; Angelo Susi; Stefano Tonetta; Marco Roveri,
    in «SOFTWARE AND SYSTEMS MODELING»,
    vol. 10,
    n. 2,
    2011
    , pp. 147 -
    160
  2. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    Safety, Dependability and Performance Analysis of Extended AADL Models,
    in «COMPUTER JOURNAL»,
    vol. 54,
    n. 5,
    2011
    , pp. 754 -
    775
  3. 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
  4. Alessandro Cimatti; Sergio Mover; Marco Roveri; Stefano Tonetta,
    From Sequential Extended Regular Expressions to NFA with Symbolic Labels,
    Proceedings of 15th Int. Conference on Implementation and Application of Automata,
    vol.6482,
    2011
    , pp. 87-
    94
    , (CIAA 2010,
    Winnipeg, Canada,
    12-15/08/2010)
  5. Alessandro Cimatti; Iman Narasamdya; Marco Roveri,
    Boosting Lazy Abstraction for SystemC with Partial Order Reduction,
    Proceedings of 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)
  6. Alessandro Cimatti; Sergio Mover; Stefano Tonetta,
    Efficient Scenario VeriFIcation for Hybrid Automata,
    2011
    , (Accepted at CAV 2011 - 23rd International Conference onComputer Aided Verification,
    Cliff Lodge, Snowbird, Utah,
    14-20/07/2011)
  7. 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)
  8. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Andrei Tchaltsev,
    A Comprehensive Approach to On-Board Autonomy Verification and Validation,
    AAAI (Conference on Artificial Intelligence)
    Press
    ,
    2011
    , (IJCAI 2011,
    Barcelona, Catalonia (Spain),
    16-22/07/2011)
  9. Daniele Campana; Alessandro Cimatti; Iman Narasamdya; Marco Roveri,
    2011
    , (18th Int. Workshop on Model Checking of Software - SPIN,
    Cliff Lodge, Snowbird, Utah,
    14–15/07/2011)
  10. A. Cimatti; S. Mover; S. Tonetta,
    Proving and Explaining the Unfeasibility of Message Sequence Charts for Hybrid Systems,
    FMCAD '11 Proceedings of the International Conference on Formal Methods in Computer-Aided Design,
    IEEE,
    n. 11,
    2011
    , pp. 54-
    62
    , (Formal Methods in Computer Aided Design (FMCAD),
    Austin, Texas, USA,
    30/10/2011)
  11. M. Bozzano; A. Cimatti; O. Lisagor; C. Mattarei; S. Mover; M. Roveri; S. Tonetta,
    Model Checking and Safety Assessment of Altarica models,
    in «ELECTRONIC COMMUNICATIONS OF THE EASST»
    Proceedings of the 11th International Workshop on Automated Verification of Critical Systems (AVoCS 2011),
    Berlin,
    EASST,
    vol.46,
    2011
    , (AVOCS 2011 - 11th International Workshop on Automated Verification of Critical Systems,
    Newcastle, UK,
    da 09/12/2011 a 09/14/2011)
  12. Roberto Cavada; Alessandro Cimatti; Andrea Micheli; Marco Roveri; Angelo Susi; Stefano Tonetta,
    OthelloPlay: a plug-in based tool for requirement formalization and validation,
    Proceedings of the 1st Workshop on Developing Tools as Plug-ins,
    2011
    , pp. 59-
    59
    , (TOPI 2011,
    Honolulu, Hawaii, USA,
    da 05/28/2011 a 05/28/2011)
  13. Alessandro Cimatti; Sergio Mover; Stefano Tonetta,
    HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction,
    2011
    , (37th EUROMICRO Conference on Software Engineering and Advanced Applications, SEAA 2011,
    Oulu, Finland,
    da 08/30/2011 a 09/02/2011)
  14. Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Xavier Olive,
    Symbolic Synthesis of Observability Requirements for Diagnosability,
    Proceedings of 11th Symposium on Advanced Space Technologies in Robotics and Automation,
    Noordwijk,
    2011
    , (ASTRA 2011,
    Noordwijk, The Netherlands,
    12/04/2011 – 14/04/2011)
  15. Robin Steel; Alexander Hoffman; Alessandro Cimatti; Marco Roveri; Konstantinos Kapellos; Alessandro Donati; Nicola Policella,
    Innovative Rover Operations Concepts–Autonomous Planning: Keeping a dog on the lead,
    International Workshop on Planning and Scheduling for Space, IWPSS 2011,
    2011
    , (International Workshop on Planning and Scheduling for Space, IWPSS 2011,
    Freiburg, Germany,
    Giugno 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,
    SPIN,
    Berlin, Heidelberg,
    Springer-Verlag,
    2010
    , pp. 1 -
    3
  3. 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)
  4. 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)
  5. Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta,
    Formalization and Validation of Safety-Critical Requirements,
    Proceedings of the Workshop on Formal Methods for Aerospace,
    vol.20,
    2010
    , pp. 68-
    75
    , (FMA'09 - 16th Int. Symposium on Formal Methods FM'09,
    Eindhoven, The Netherlands,
    03/11/2009)
  6. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri; Ralf Wimmer,
    A Model Checker for AADL,
    Proceedings of 22nd International Conference on Computer Aided Verification,
    Springer,
    vol.6174,
    2010
    , pp. 562-
    565
    , (CAV 2010,
    Edinburgh, UK,
    15-19/07/2010)
  7. Roderick Bloem; Alessandro Cimatti; Karin Greimel; Georg Hofferek; Robert Koenighofer; Marco Roveri; Viktor Schuppan; Richard Seeber,
    RATSY - A new Requirements Analysis Tool with Synthesis,
    Proceedings of 22nd Int. Conference on Computer Aided Verification,
    Springer,
    vol.6174,
    2010
    , pp. 425-
    429
    , (CAV 2010,
    Edinburgh, UK,
    15-19/07/2010)
  8. Lei Bu; Alessandro Cimatti; Xuandong Li; Sergio Mover; Stefano Tonetta,
    Model Checking of Hybrid Systems using Shallow Synchronization,
    Proceedings of 30th IFIP Int. Conference on FORmal TEchniques for Networked and Distributed Systems, part of DisCoTec'10,
    vol.6117,
    2010
    , pp. 155-
    169
    , (FORTE 2010,
    Amsterdam, The Netherlands,
    07-10/06/2010)
  9. Angelo Chiappini; Alessandro Cimatti; Luca Macchi; Oscar Rebollo; Marco Roveri; Angelo Susi; Stefano Tonetta; Berardino Vittorini,
    Formalization and validation of a subset of the European Train Control System,
    Proceedings of 32nd Int. Conference on Software Engineering,
    New York,
    vol.2,
    2010
    , pp. 109-
    118
    , (ICSE (2),
    Cape Town, South Africa,
    01-08/05/2010)
  10. Alessandro Cimatti; Andrea Micheli; Iman Narasamdya; Marco Roveri,
    Verifying SystemC: a Software Model Checking Approach,
    Proceedings of the 10th Int. Conference on Formal Methods in Computer-Aided Design,
    2010
    , pp. 51-
    60
    , (FMCAD 2010,
    Lugano, Switzerland,
    October, 20-23, 2010)
  11. Anders Franzen; Alessandro Cimatti; Alexander Nadel; Roberto Sebastiani; Jonathan Shalev,
    Applying SMT in Symbolic Execution of Microcode,
    Proceedings of 10th Int. Conference on Formal Methods in Computer-Aided Design,
    ACM Press, IEEE Press,
    2010
    , pp. 121-
    128
    , (FMCAD 2010,
    Lugano, Switzerland,
    20-23/10/2010)
  12. Marco Bozzano; Roberto Cavada; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Xavier Olive,
    Formal Verification and Validation of AADL Model,
    2010
    , (ERTS² 2010 - Embedded Real Time Software and Systems,
    Toulouse, France,
    19-21/05/2010)
  13. Thi Thieu Hoa Le; Luigi Palopoli; Roberto Passerone; Yusi Ramadian; Alessandro Cimatti,
    Parametric Analysis of Distributed Firm Real-Time Systems: A Case Study,
    Proceedings of the 15th Int. Conference on Emerging Technologies and Factory Automation,
    2010
    , (ETFA10,
    Bilbao, Spain,
    13-16/09/2010)
  14. Marco Roveri; Alessandro Cimatti; Iman Narasamdya; Andrea Micheli; Daniele Campana; Alberto Griggio; Andrei Tchaltsev,
    2010,
  15. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri; Ralf Wimmer; Roberto Cavada,
    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. Alessandro Cimatti; Marco Roveri; Stefano Tonetta,
    Requirements Validation for Hybrid Systems,
    Proceedings 21st Int. Conference on Computer Aided Verification,
    Springer,
    vol.5643,
    2009
    , pp. 188-
    203
    , (CAV 2009,
    Grenoble, France,
    26/06/2009-02/07/2009)
  4. Alessandro Cimatti; Jori Juhani Dubrovin; Tommi Antero Junttila; Marco Roveri,
    Proceedings of the Formal Methods in Computer Aided Design,
    2009
    , pp. 9-
    16
    , (FMCAD 2009,
    AUSTIN, TX, USA,
    15/11/2009 - 18/11/2009)
  5. 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)
  6. Roberto Cavada; Alessandro Cimatti; Alessandro Mariotti; Cristian Mattarei; Andrea Micheli; Sergio Mover; Marco Pensallorto; Marco Roveri; Angelo Susi; Stefano Tonetta,
    Supporting Requirements Validation: The EuRailCheck Tool,
    Proceedings of 24th Int. Conference Automated Software Engineering,
    2009
    , pp. 665-
    667
    , (ASE 2009,
    Auckland, New Zealand,
    16/11/2009 - 20/11/2009)
  7. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Andrei Tchaltsev,
    Workshop on Verification and Validation of Planning and Scheduling Systems,
    2009
    , pp. 1-
    10
    , (VV&PS 2009 - ICAPS,
    Thessaloniki, Greece,
    20/09/2009)
  8. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems,
    Proceedings of 28th Int. International Conference on Computer Safety, Reliability and Security,
    Springer,
    vol.5775,
    2009
    , pp. 173-
    186
    , (SAFECOMP 2009,
    Hamburg, Germany,
    15-18/09/2009)
  9. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll,
    Verification and performance evaluation of AADL models,
    Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering,
    New York,
    ACM,
    2009
    , pp. 285-
    286
    , (ESEC/FSE 2009,
    Amsterdam, The Netherlands,
    24-28/08/2009)
  10. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    Proceedings 2nd Int. Workshop on Model Based Architecting and Construction of Embedded Systems,
    CEUR-WS.org,
    vol.507,
    2009
    , pp. 87-
    91
    , (ACESMB09,
    Denver, Colorado, USA,
    06/10/2009)
  11. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll,
    Codesign of Dependable Systems: A Component-Based Modeling Language,
    Proceedings of the 7th IEEE/ACM Int. Conference on Formal Methods and Models for Codesign,
    Piscataway, NJ,
    2009
    , pp. 121-
    130
    , (MEMOCODE'09,
    Cambridge, Massachusetts, USA,
    13-15/07/2009)
  12. Marco Roveri; Alessandro Cimatti; Viktor Schuppan; Andrei Tchaltsev; Roberto Cavada,
    2009,
  13. Dirk Beyer; Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani,
    Software Model Checking via Large-Block Encoding,
    2009
  14. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    Codesign of Dependable Systems: A Component-Based Language,
    2009
  15. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems,
    2009
  16. 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
  17. 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. Alessandro Cimatti; Marco Roveri; Stefano Tonetta,
    Symbolic Compilation of PSL,
    in «IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS»,
    vol. 27,
    n. 10,
    2008
    , pp. 1737 -
    1750
  2. Alessandro Cimatti; Marco Pistore; Paolo Traverso,
    Automated Planning,
    Handbook of Knowledge Representation,
    Elsevier,
    2008
    , pp. 841 -
    867
  3. 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)
  4. 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)
  5. Alessandro Cimatti; Marco Roveri; Viktor Schuppan; Andrei Tchaltsev,
    Diagnostic Information for Realizability,
    Proceedings of 9th Int. Conference Verification, Model Checking, and Abstract Interpretation,
    Springer,
    vol.4905,
    2008
    , pp. 52-
    67
    , (VMCAI 2008,
    San Francisco, USA,
    07/01/2008-09/01/2008)
  6. Alessandro Cimatti,
    Beyond Boolean SAT: Satisfiability Modulo Theories,
    Proceedings of the 9th Int. Workshop on Discrete Event Systems,
    IEEE Press,
    2008
    , pp. 68-
    73
    , (WODES 2008,
    Goteborg, Sweden,
    28/05/2008 - 30/05/2008)
  7. Alessandro Cimatti; Luigi Palopoli; Yusi Ramadian,
    Symbolic Computation of Schedulability Regions using parametric timed automata,
    Proceeding of the 29th IEEE Real-Time Systems Symposium,
    Washington, DC,
    IEEE Computer Society,
    2008
    , pp. 80-
    89
    , (RTSS '08,
    Barcelona, Spain,
    30/11/2008 - 03/12/2008)
  8. Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta,
    Object Models with Temporal Constraints,
    Proceedings 6th Int. Conference on Software Engineering and Formal Methods,
    2008
    , pp. 249-
    258
    , (SEFM 2008,
    Cape Town,
    10/11/2008 - 14/11/2008)
  9. Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta,
    From Informal Requirements to Property-Driven Formal Validation,
    Proceedings of 13th Int. Workshop on Formal Methods for Industrial Critical Systems,
    Springer Verlag,
    vol.5596,
    2008
    , pp. 166-
    181
    , (FMICS 2008,
    L’Aquila, Italy,
    15/09/2008 - 16/09/2008)
  10. Marco Bozzano; Alessandro Cimatti; Andrea Guiotto; Andrea Martelli; Marco Roveri; Andrei Tchaltsev; Yuri Yushtein,
    On-Board Autonomy via Symbolic Model Based Reasoning,
    Proceedings of 10th Workshop on Advanced Space Technologies for Robotics and Automation,
    Noordwijk,
    2008
    , (ASTRA 2008,
    Noordwijk, The Netherlands,
    11/11/2008 - 13/11/2008)
  11. Alessandro Cimatti; Andrea Guiotto; Marco Roveri,
    On Board Model Checking for Space Applications,
    Proceedings of ESA Workshop on Avionics Data, Control and Software Systems,
    Noordwijk,
    2008
    , pp. 10-
    11
    , (ADCSS,
    Noordwijk, The Netherlands,
    29/10/2008 - 31/10/2008)
  12. Alessandro Cimatti; Robert B. Jones (eds.),
    Formal Methods in Computer-Aided Design, Portland, Oregon, USA, 17-20 November 2008,
    Piscataway, NJ,
    IEEE,
    2008
  13. Alessandro Cimatti; Marco Bozzano; Adolfo Villafiorita,
    2008,

2007

  1. Roderick Bloem; Alessandro Cimatti; Ingo Pill; Marco Roveri,
    Symbolic Implementation of Alternating Automata,
    in «INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE»,
    vol. 18,
    n. 4,
    2007
    , pp. 727 -
    743
  2. Piergiorgio Bertoli; Marco Bozzano; Alessandro Cimatti,
    A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis,
    Model Checking and Artificial Intelligence,
    Berlin, Heidelberg,
    Springer-Verlag,
    2007
    , pp. 1 -
    18
  3. Marco Bozzano; Alessandro Cimatti; Francesco Tapparo,
    Symbolic Fault Tree Analysis for Reactive Systems,
    5th Int. Symposium on Automated Technology for Verification and Analysis,
    Springer-Verlag,
    vol.4762,
    2007
    , pp. 162-
    176
    , (ATVA 2007,
    Tokyo, Japan,
    22-25/10/2007)
  4. Zvonimir Rakamaric; Roberto Bruttomesso; Alan J. Hu; Alessandro Cimatti,
    Verifying Heap-Manipulating Programs in an SMT Framework,
    5th Int. Symposium on Automated Technology for Verification and Analysis,
    Springer-Verlag,
    vol.4762,
    2007
    , pp. 237-
    252
    , (ATVA 2007,
    Tokyo, Japan,
    22-25/10/2007)
  5. Alessandro Cimatti; Marco Roveri; Viktor Schuppan; Stefano Tonetta,
    Boolean Abstraction for Temporal Logic Satisfiability,
    Proceedings of 19th Int. Conference Computer Aided Verification,
    Springer,
    vol.4590,
    2007
    , pp. 532-
    546
    , (CAV,
    Berlin, Germany,
    03/07/2007-07/07/2007)
  6. 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)
  7. Roberto Cavada; Alessandro Cimatti; Anders Franzen; Kalyanasundaram Krishnamani; Marco Roveri; R. K. Shyamasundar,
    Computing Predicate Abstractions by Integrating BDDs and SMT Solvers,
    Proceedings of the Formal Methods in Computer Aided Design,
    Washington, DC,
    2007
    , pp. 69-
    76
    , (FMCAD '07,
    Austin, Texas,
    11/11/2007-14/11/2007)
  8. 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)
  9. Alessandro Cimatti; Marco Roveri; Stefano Tonetta,
    Syntactic Optimizations for PSL Verification,
    Proceedings of 13th Int. Conference Tools and Algorithms for the Construction and Analysis of Systems,
    Springer,
    vol.4424,
    2007
    , pp. 505-
    518
    , (TACAS,
    Braga, Portugal,
    24/03/2007-01/04/2007)
  10. Roberto Bruttomesso; Alessandro Cimatti; Roberto Sebasatiani; Alberto Griggio; Anders Franzen,
    2007,

2006

  1. P. Bertoli; A. Cimatti; M. Roveri; P. Traverso,
    Strong Planning under Partial Observability,
    in «ARTIFICIAL INTELLIGENCE»,
    vol. 170,
    n. 4-5,
    2006
    , pp. 337 -
    384
  2. Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Silvio Ranise; Peter van Rossum; Roberto Sebastiani,
    Efficient theory combination via boolean search,
    in «INFORMATION AND COMPUTATION»,
    vol. 204,
    n. 10,
    2006
    , pp. 1493 -
    1525
  3. Alessandro Cimatti; Roberto Sebastiani,
    Formal Methods for Hardware Verification,
    Berlin, Heidelberg,
    Springer,
    2006
    , pp. 144 -
    175
  4. Alessandro Armando; Alessandro Cimatti,
    Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005).
    Elsevier B.V.,
    2006
    , pp. 1 -
    2
  5. Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Anders Franzen; Ziyad Hanna; Zurab Khasidashvili; Amit Palti; Roberto Sebastiani,
    Proceedings of 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning,
    vol.144, issue 2,
    2006
    , pp. 3-
    14
    , (PDPAR 2005 affiliated workshop to CAV'05,
    University of Edinburgh, Scotland, UK,
    12/07/2005)
  6. R. Bloem; A. Cimatti; I. Pill; M. Roveri; S. Semprini,
    Symbolic Implementation of Alternating Automata,
    Proceedings of 11th Int. Conference Implementation and Application of Automata,
    Springer,
    vol.4094,
    2006
    , pp. 208-
    218
    , (CIAA,
    Taipei, Taiwan,
    21/08/2006-23/08/2006)
  7. I. Pill; S. Semprini; R. Cavada; M. Roveri; R. Bloem; A. Cimatti,
    Formal analysis of hardware requirements,
    Proceedings of 43rd annual Design Automation Conference,
    New York, NY,
    2006
    , pp. 821-
    826
    , (DAC,
    San Francisco, USA,
    24/07/2006-28/07/2006)
  8. P. Bertoli; A. Cimatti; M. Pistore,
    Strong Cyclic Planning Under Partial Observability,
    Proceedings of 17th European Conference on Artificial Intelligence,
    Amsterdam,
    2006
    , pp. 580-
    584
    , (ECAI 2006,
    Riva del Garda, Italy,
    29/08/2006-01/09/2006)
  9. Roderick Bloem; Alessandro Cimatti; Ingo Pill; Marco Roveri; Simone Semprini; Andrei Tchaltsev,
    RAT: A tool for formal analysis of requirements,
    Demo Session of the 17th European Conference on Artificial Intelligence,
    2006
    , (ECAI,
    Riva del Garda, Italy,
    28/08/2006-01/09/2006)
  10. Alessandro Cimatti; Marco Roveri; Simone Semprini; Stefano Tonetta,
    From PSL to NBA: a Modular Symbolic Encoding,
    Proceedings of 6th Int. Conference on Formal Methods in Computer Aided Design,
    2006
    , pp. 125-
    133
    , (FMCAD,
    San Jose, CA, USA,
    12/11/2006-16/11/2006)
  11. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore,
    Towards strong cyclic planning under partial observability,
    Proceedings of the 16th Int. Conference on Automated Planning and Scheduling,
    2006
    , pp. 354-
    357
    , (ICAPS’06,
    Cumbria, UK,
    6-10/06/2006)
  12. 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)
  13. 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)
  14. Marco Bernardo; Alessandro Cimatti (eds.),
    Berlin Heidelberg New York,
    Springer,
    2006
  15. Armando A.; Cimatti A. (eds.),
    Post-workshop Proceedings of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning,
    Electronic Notes in Theoretical Computer Science -- Elsevier,
    2006

2005

  1. Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi Junttila; Peter van Rossum; Stephan Schulz; Roberto Sebastiani,
    Mathsat: Tight Integration of SAT and Mathematical Decision Procedures,
    in «JOURNAL OF AUTOMATED REASONING»,
    vol. 35,
    n. 1-3,
    2005
    , pp. 265 -
    293
  2. M. Bozzano; R. Bruttomesso; A. Cimatti; T. A. Junttila; Rossum Peter van; S. P. Schulz; R. Sebastiani,
    An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic,
    Proceedings of 11th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems,
    Springer,
    vol.3440,
    2005
    , pp. 317-
    333
    , (TACAS 2005,
    Edinburgh, UK,
    04/04/2005 - 08/04/2005)
  3. Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Peter van Rossum; Stephan Peter Schulz; Roberto Sebastiani,
    The Mathsat3 System,
    Proceedings of 20th Int. Conference on Automated Deduction,
    Springer,
    vol.3632,
    2005
    , pp. 315-
    321
    , (CADE-20,
    Tallin, Estonia,
    22-27/07/2005)
  4. Gilles Audemard; Marco Bozzano; Alessandro Cimatti; Roberto Sebastiani,
    Verifying Industrial Hybrid Systems with MathSAT,
    Proceedings of 2nd Int. Workshop on Bounded Model Checking,
    Elsevier B.V.,
    vol.119, issue 2,
    2005
    , pp. 17-
    32
    , (BMC 2004,
    Boston, MA, USA,
    18/07/2004)
  5. Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi Junttila; Silvio Ranise; Peter van Rossum; Roberto Sebastiani,
    Efficient Satisfiability Modulo Theories via Delayed Theory Combination,
    Proceeding of 17th Int. Conference on Computer Aided Verification,
    Springer,
    vol.3576,
    2005
    , pp. 335-
    349
    , (CAV,
    University of Edinburgh, Scotland, UK,
    6-10/07/2005)
  6. Marco Roveri; Alessandro Cimatti; Andrei Tchaltsev; Roberto Cavada; Simone Semprini; Roderick Bloem; Ingo Pill,
    2005,
  7. M. Bozzano; R. Bruttomesso; A. Cimatti; T. Antero Junttila; S. Ranise; Rossum Peter van; R. Sebastiani,
    Efficient Theory Combination via Boolean Search,
    Many approaches to the decision of quantifier free formulae with respect to a background theory T - also known as Satisfiability Modulo Theory, or SMT(T) - rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory is the combination T1 U T2 of two simpler theories, the approach is typically instantiated by means of a combination schema (e.g. Nelson-Oppen, Shostak).
    In this paper we propose a new approach to SMT(T1 U T2), where the enumerator of truth assignments is integrated with two decision procedures for T1 and for T2, which act independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the purified formula, but also to all the equalities between interface variables.
    This approach is simple and expressive: for instance, no modification is required to handle non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art boolean and SMT search techniques, and on theory layering (i.e. cheaper reasoning first, and more often).
    We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions (EUF) and Linear Arithmetic (LA), both for (the convex case of) reals and for (the non-convex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with competitor tools, obtaining speed-ups up to two orders of magnitude
    ,
    2005
  8. M. Bozzano; R. Bruttomesso; A. Cimatti; T. A. Junttila; R. Peter van; S. P. Schulz; R. Sebastiani,
    MathSAT: Thigt Integration of SAT and Mathematical Decision Procedures,
    Recent improvements in propositional satisfiability techniques (SAT) made it possible to tackle successfully some hard real-world problems (e.g. model-checking, circuit testing, propositional planning) by encoding into SAT.
    However, a purely boolean representation is not expressive enough for many other real-world applications, including the verification of timed and hybrid systems, of proof obligations in software, and of circuit design at RTL level. These problems can be naturally modeled as satisfiability in Linear Arithmetic Logic (LAL), i.e., the boolean combination of propositional variables and linear constraints over numerical variables.
    In this paper we present mathsat, a new, SAT-based decision procedure for LAL, based on the (known approach) of integrating a state-of-the-art SAT solver with a dedicated mathematical solver for LAL. We improve mathsat in two different directions.
    First, the top level procedure is enhanced, and now features a tighter integration between the boolean search and the mathematical solver. In particular, we allow for theory-driven backjumping and learning, and theory-driven deduction; we use static learning in order to reduce the number of boolean models that are mathematically inconsistent; we exploit problem clustering in order to partition mathematical reasoning; and we define a stack-based interface that allows us to implement mathematical reasoning in an incremental and backtrackable way.
    Second, the mathematical solver is based on layering, i.e. the consistency of (partial) assignments is checked in theories of increasing strength (equality and uninterpreted functions, linear arithmetic over the reals, linear arithmetic over the integers). For each of these layers, a dedicated (sub)solver is used. Cheaper solvers are called first, and detection of inconsistency makes calls of the subsequent solvers superfluous.
    We provide a thorough experimental evaluation of our approach, by taking into account a large set of previously proposed benchmarks. We first investigate the relative benefits and drawbacks of each proposed technique by comparison with respect to a reference option setting. We then demonstrate the global effectiveness of our approach by a comparison with several state-of-the-art decision procedures. We show that the behavior of mathsat is often superior to its competitors, both on LAL, and in the subclass of Difference Logic
    ,
    2005
  9. M. Bozzano; R. Brutomesso; A. Cimatti; T. A. Junttila; S. Ranise; Rossen Peter van; R. Sebastiani,
    Efficient Satisfiability Modulo Theories via Delayed Theory Combination,
    The problem of deciding the satisfiability of a quantifier-free formula with respect to a background theory, also known as Satisfiability Modulo Theories (smt), is gaining increasing relevance in verification: representation capabilities beyond propositional logic allow for a natural modeling of real-world problems (e.g., pipeline and RTL circuits verification, proof obligations in software systems).
    In this paper, we focus on the case where the background theory is the combination T1 U T2 of two simpler theories. Many smt procedures combine a boolean model enumeration with a decision procedure for T1 U T2, where conjunctions of literals can be decided by an integration schema such as Nelson-Oppen, via a structured exchange of interface formulae (e.g., equalities in the case of convex theories, disjunctions of equalities otherwise).
    We propose a new approach for SMT(T1 U T2), called Delayed Theory Combination, which does not require a decision procedure for T1 U T2, but only individual decision procedures for T1 and T2, which are directly integrated to the boolean model enumerator.
    This approach is much simpler and natural, allows each of the solvers to be implemented and optimized without taking into account the others, and it nicely encompasses the case of non-convex theories.
    We show the effectiveness of the approach by a thorough experimental comparison
    ,
    2005

2004

  1. Alessandro Cimatti; Marco Roveri; Piergiorgio Bertoli,
    Conformant Planning via Symbolic Model Checking and Heuristic Search,
    in «ARTIFICIAL INTELLIGENCE»,
    vol. 159,
    n. 1-2,
    2004
    , pp. 127 -
    206
  2. P. Bertoli; A. Cimatti; P. Traverso,
    Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains,
    Proceedings of 16th Eureopean Conference on Artificial Intelligence,
    2004
    , pp. 657-
    661
    , (ECAI'2004,
    Valencia, Spain,
    22/08/2004 - 27/08/2004)
  3. A. Cimatti; M. Roveri; D. Sheridan,
    Bounded Verification of Past LTL,
    Proceedings of 5th Int. Conference on Formal Methods in Computer-Aided Design,
    Springer,
    vol.3312,
    2004
    , pp. 245-
    259
    , (FMCAD,
    Austin, Texas, USA,
    14/11/2004-17/11/2004)
  4. F. Roelofsen; L. Serafini; A. Cimatti,
    Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems,
    Proceedings of 16th Eureopean Conference on Artificial Intelligence,
    2004
    , pp. 58-
    62
    , (ECAI'2004,
    Valencia, Spain,
    22/08/2004-27/08/2004)
  5. Marco Bozzano; Alessandro Cimatti; Gabriele Colombini; Veselin Kirov; Roberto Sebastiani,
    The MathSAT solver -- a progress report,
    Proceeding of 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning,
    2004
    , (PDPAR,
    University College Cork, Ireland,
    05/07/2004)
  6. M. Bozzano; A. Cimatti; G. Colombini; V. Kirov; R. Sebastiani,
    The MAthSAT Solver. A progress report,
    Many problems of practical relevance are conveniently expressed as boolean combinations of propositional variables and mathematical constraints. The development of decision procedures able to check the satisfiability of such formulas is therefore being devoted an increasing interest.
    The MathSat family of deciders is based on the extension of a DPLL propositional satisfiability procedure, used as an assignment enumerator. MathSat pioneers a lazy and layered approach, where propositional reasoning is tightly integrated with solvers of increasing expressive power (e.g. to reason about equality and linear arithmetic) in such a way that ``more expensive'' layers are called less frequently.
    In this paper, we show the advances in the development of MathSat. We discuss the implications related to the use of Minisat, a new-generation propositional SAT solver; the role of an incremental mathematical reasoner; the role of static learning; and the extension to integer variables. We show that the new version of MathSat is significantly more efficient than the previous one
    ,
    2004
  7. Marco Bozzano; R. Bruttomesso; A. Cimatti; R. Sebastiani,
    The MathSAT Solver - a comparative evaluation,
    Many problems of practical relevance are conveniently expressed as boolean combinations of propositional variables and mathematical constraints. The development of decision procedures able to check the satisfiability of such formulas is therefore being devoted an increasing interest. The MathSat family of deciders is based on the extension of a DPLL propositional satisfiability procedure, used as an assignment enumerator. MathSat pioneers a lazy and layered approach, where propositional reasoning is tightly integrated with solvers of increasing expressive power (e.g. to reason about equality and linear arithmetic) in such a way that "more expensive" layers are called less frequently.
    In this paper, we discuss the advances in the development of MathSat. In particular, the current version of the tool is built on minisat, a new-generation propositional SAT solver, and Cassowary, an incremental mathematical reasoner, and it incorporates support for integer variables. We compare the performance of MathSat with CVCL and show that MathSat is significantly more efficient on a set of benchmarks related to word-level verification
    ,
    2004

2003

  1. Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso,
    Weak, Strong, and Strong Cyclic Planning via Symbolic Model Checking,
    in «ARTIFICIAL INTELLIGENCE»,
    vol. 147,
    n. 1-2,
    2003
  2. Armin Biere; Alessandro Cimatti; E.M. Clarke; Ofer Strichman; Yunshan Zhu,
    Bounded Model Checking,
    in «ADVANCES IN COMPUTERS»,
    vol. 58,
    n. ISBN 0-12-012158-1,
    2003
    , pp. 118 -
    149
  3. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Paolo Traverso,
    Proceedings of ICAPS`03 - 13th International Conference on Automated Planning and Scheduling,
    AAAI,
    2003
    , pp. 215-
    225
    , (Proceedings of ICAPS`03 - 13th International Conference on Automated Planning and Scheduling,
    Trento, Italy,
    09/06/2003 - 13/06/2003)
  4. Marco Bozzano; Adolfo Villafiorita; O. Akerlund; P. Bieber; C. Bougnol; E. Boede; M. Bretschneider; A. Cavallo; C. Castel; M. Cifaldi; Alessandro Cimatti; A. Griffault; C. Kehren; B. Lawrence; A. Luedtke; S. Metge; C. Papadopoulos; R. Passarello; T. Peikenkamp; P. Persson; C. Seguin; L. Trotta; L. Villafiorita A. Valacca; Gabriele Zacco,
    ESACS: an integrated methodology for design and safety analysis of complex systems,
    Safety & Reliability - ESREL 2003 - Proceedings of the European Safety and Reliability Conference 2003,
    Balkema,
    2003
    , (Safety & Reliability - ESREL 2003 - Proceedings of the European Safety and Reliability Conference 2003,
    Maastricht, The Netherlands,
    2003)
  5. Piergiorgio Bertoli; Alessandro Cimatti; Paolo Traverso,
    ICAPS`03 Workshop on Planning under Uncertainty and Incomplete Information,
    AAAI,
    2003
    , pp. 1-
    7
    , (ICAPS`03 Workshop on Planning under Uncertainty and Incomplete Information,
    Trento, Italy,
    09/06/2003 - 13/06/2003)
  6. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso,
    ICAPS`03: system demo session,
    2003
    , (ICAPS`03: system demo session,
    2003)
  7. Piergiorgio Bertoli; Alessandro Cimatti; Lago U. Dal; Marco Pistore,
    ICAPS`03 Workshop on PDDL,
    2003
    , pp. 15-
    24
    , (ICAPS`03 Workshop on PDDL,
    Trento, Italy,
    2003)
  8. Marco Benedetti; Alessandro Cimatti,
    Bounded Model Checking for past LTL,
    Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of the 9th International Conference, TACAS 2003,
    Springer,
    vol.2619,
    2003
    , pp. 18-
    33
    , (Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of the 9th International Conference, TACAS 2003,
    2003)
  9. Alessandro Cimatti; Charles Pecheur; Roberto Cavada,
    Formal Verification of Diagnosability via Symbolic Model Checking,
    IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence,
    Morgan Kaufmann,
    2003
    , pp. 363-
    369
    , (IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence,
    Acapulco, Mexico,
    2003)
  10. Gilles Audemard; Marco Bozzano; Alessandro Cimatti; Roberto Sebastiani,
    CADE-19 Workshop: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR`03),
    2003
    , pp. 62-
    76
    , (CADE-19 Workshop: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR`03),
    Miami, USA,
    2003)
  11. Piergiorgio Bertoli; Alessandro Cimatti; Lago U. Dal; Marco Pistore,
    Extending PDDL to mondeterminism, limited sensing and iterative conditional plans,
    The last decade has witnessed a dramatic progress in the variety and performance of techniques and tools for classical planning. Much of this can be ascribed to the existence of a de-facto standard modeling language for classical planning, PDDL. PDDL has fostered information sharing and data exchange in the planning community, and has made international classical planning competitions possible. At the same time, in the last few years, non-classical planning has gained considerable attention, due to its capability to capture relevant features of real-life domains which the classical framework fails to express. However, no significant effort has been made to achieve a standard means for expressing non-classical problems, making it difficult for the planning community to compare non-classical approaches and systems. This paper provides a contribution in this direction. We extend PDDL in order to express three very relevant features outside classical planning: uncertainty in the initial state, nondeterministic actions, and partial observability. NPDDL's extensions are designed to retain backward compatibility with PDDL, and with an emphasis on compactness of the representation. Moreover, we define a powerful, user-friendly plan language to go together with NPDDL. The language allows expressing program-like plans with branching and iterations structures, as it is necessary to solve planning problems in the presence of initial state uncertainty, nondeterminism and partial observability. We are testing NPDDL's ability to cope with a variety of problems, as they are handled by a state-of-the-art planner, MBP,
    2003
  12. Alessandro Cimatti; C. Pecheur; Roberto Cavada,
    Formal Verification of Diagnosability via Symbolic Model Checking,
    This paper addresses the formal verification of diagnosis systems. We tackle the problem of diagnosability: given a partially observable dynamic system, and a diagnosis system observing its evolution over time, we discuss how to verify (at design time) if the diagnosis system will be able to infer (at run-time) the required information on the hidden part of the dynamic state. We tackle the problem by looking for pairs of scenarios that are observationally indistinguishable, but lead to situations that are required to be distinguished. We reduce the problem to a model checking problem. The finite state machine modeling the dynamic system is replicated to construct such pairs of scenarios; the diagnosability conditions are formally expressed in temporal logic; the check for diagnosability is carried out by solving a model checking problem. We ocus on the practical applicability of the method. We show how the formalism is adequate to represent diagnosability problems arising from a significant, real-world application. Symbolic model checking techniques are used to formally verify and check incrementally refine the diagnosability conditions,
    2003

2002

  1. Alessandro Cimatti; Marco Pistore; Marco Roveri; Roberto Sebastiani,
    Improving the encoding of LTL Model Checking into SAT,
    VMCAI-2002 Workshop on Verification Model Checking and Abstract Interpretation,
    Springer,
    vol.2294,
    2002
    , pp. 196-
    207
    , (VMCAI-2002 Workshop on Verification Model Checking and Abstract Interpretation,
    2002)
  2. Gilles Audemard; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani,
    Bounded Model Checking for Timed Systems,
    Formal Techniques for Networked and Distributed Systems - FORTE 2002. Proceedings of the 22nd IFIP TC6 WG 6.1 International Conference,
    Springer,
    2002
    , pp. 243-
    259
    , (Formal Techniques for Networked and Distributed Systems - FORTE 2002. Proceedings of the 22nd IFIP TC6 WG 6.1 International Conference,
    Houston, Texas, USA,
    2002)
  3. Alessandro Cimatti; E. Giunchiglia; Marco Roveri; Marco Pistore; Roberto Sebastiani; A. Tacchella,
    Integrating BDD-based and SAT-based Symbolic Model Checking,
    Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002,
    Springer,
    vol.2309,
    2002
    , pp. 49-
    56
    , (Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002,
    Santa Margherita Ligure, Italy,
    2002)
  4. Piergiorgio Bertoli; Alessandro Cimatti; J. Slaney; S. Thiebaux,
    Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking,
    15th Eureopean Conference on Artificial Intelligence (ECAI 2002),
    IOS Press,
    2002
    , pp. 576-
    580
    , (15th Eureopean Conference on Artificial Intelligence (ECAI 2002),
    Lyon, France,
    2002)
  5. Gilles Audemard; Piergiorgio Bertoli; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani,
    CADE-18 Conference on Automated Deduction,
    Springer,
    2002
    , pp. 195-
    210
    , (CADE-18 Conference on Automated Deduction,
    Copenhagen, Denmark,
    2002)
  6. Gilles Audemard; Piergiorgio Bertoli; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani,
    CALCULEMUS-2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning,
    2002
    , pp. 157-
    192
    , (CALCULEMUS-2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning,
    Marseille, France,
    2002)
  7. Alessandro Cimatti; E.M. Clarke; Enrico Giunchiglia; Fausto Giunchiglia; Marco Pistore; Marco Roveri; Roberto Sebastiani; A. Tacchella,
    NuSMV 2: An OpenSource Tool for Symbolic model Checking,
    CAV 2002, Conference on Computer-Aided Verification,
    Springer,
    vol.2404,
    2002
    , pp. 359-
    364
    , (CAV 2002, Conference on Computer-Aided Verification,
    Copenhagen, Denmark,
    2002)
  8. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Paolo Traverso,
    Electronic Proceedings of AIPS`02 Workshop on Planning via Model Checking,
    2002
    , (Electronic Proceedings of AIPS`02 Workshop on Planning via Model Checking,
    2002)
  9. Marco Roveri; Alessandro Cimatti; Roberto Cavada; Andrei Tchaltsev; Andrea Micheli; Alessandro Mariotti; Sergio Mover; Marco Pensallorto; Armando Tacchella; Daniel Sheridan; Gavin Keighren; Tommi Junttila; Timo Latvala,
    2002,

2001

  1. Alessandro Cimatti; Marco Roveri; Piergiorgio Bertoli,
    Searching Porwerset Automata by Combining Explicit-State and Symbolic Model Checking,
    Tools and Algorithms for the Construction and Analysis of Systems [TACAS 2001], Conference Proceedings,
    Springer,
    vol.2031,
    2001
    , pp. 313-
    327
    , (Tools and Algorithms for the Construction and Analysis of Systems [TACAS 2001], Conference Proceedings,
    2001)
  2. Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri,
    Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning,
    17th International Joint Conference on Artificial Intelligence, IJCAI 2001,
    Morgan Kaufmann,
    2001
    , pp. 467-
    472
    , (17th International Joint Conference on Artificial Intelligence, IJCAI 2001,
    Seattle, USA,
    04/08/2001 - 10/08/2001)
  3. Alessandro Cimatti; E. Giunchiglia; Marco Pistore; Marco Roveri; Roberto Sebastiani; A. Tacchella,
    NuSMV Version 2: BDD-based + SAT-based Symbolic Model Checking,
    Proceedings of the IJCAR Workshop `Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics`,
    no publisher,
    2001
    , (Proceedings of the IJCAR Workshop `Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics`,
    Siena, Italy,
    19/06/2001)
  4. Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri,
    Conditional Planning under Partial Obserbability as Heuristic-Symbolic Search in Belief Space,
    Sixth European Conference on Planning [ECP-01],
    Springer,
    2001
    , pp. 379-
    384
    , (Sixth European Conference on Planning [ECP-01],
    2001)
  5. Massimo Benerecetti; Alessandro Cimatti,
    Symbolic model checking for multi-agent systems,
    Second Workshop on Computational Logic in Multi-Agent Systems (CLIMA`01),
    2001
    , (Second Workshop on Computational Logic in Multi-Agent Systems (CLIMA`01),
    Paphos, Cyprus,
    2001)
  6. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso,
    IJCAI-2001 Workshop on Planning under Uncertainty and Incomplete Information (PRO-2),
    2001
    , (IJCAI-2001 Workshop on Planning under Uncertainty and Incomplete Information (PRO-2),
    Seattle, Washington, USA,
    2001)
  7. Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), Proceedings,
    Morgan Kaufmann,
    2001
    , pp. 473-
    478
    , (Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), Proceedings,
    Seattle, Washington, USA,
    2001)
  8. Alessandro Cimatti,
    Industrial Applications of Model Checking,
    Formal methods have a great potential of application in the development of industrial critical systems. in certain application fields, formal methods are even becoming part of standards. Among formal methods, Model Checking is proving particularly effective, especially thanks to its ability to automatically analyze complex designs and to produce counterexamples. However, the application of formal methods in the industrial development practice is by no means trivial. Formal methods can be costly, slow down the development, and require training and changes to the development cycle. In this paper, the application of Model Checking techniques in the development of the application of Model Checking techniques in the development of industrial critical systems is discussed, by focusing on two projects where Model Checking has been successfully applied under different conditions.,
    2001
  9. Piergiorgio Bertoli; Alessandro Cimatti,
    Improving Heuristics for Planning and Search in Belief Space,
    Search in the space of beliefs has been proposed as a convenient framework for tackling planning under uncertainty. Significant improvements have been recently achieved, especially thanks to the use of symbolic model checking techniques such as Binary Decision Diagrams. However, the problem is extremely complex, and the heuristics available so far are unable to provide enough guidance for an informed search. In this paper we tackle the problem of defining effective heuristics for driving the search in belief space. The basic intuition is that the "degree of knowledge" associated with the belief states reached by partial plans must be explicitly taken into account when deciding the search direction. We propose a way of ranking belief states depending on their degree of knowledge with respect to a given set of boolean functions. This allows us to define a planning algorithm based on the identification and solution of suitable "knowledge subgoals", that are used as intermediate steps during the search. The solution of knowledge subgoals is based on the identification of "knowledge acquisition conditions", i.e. subsets of the state space from where it is possible to perform knowledge acquisition actions. We show the effectiveness of the proposed ideas by observing substantial improvements in the conformant planning algorithms of MBP,
    2001

2000

  1. Alessandro Cimatti; Marco Roveri,
    Conformant Planning via Symbolic Model Checking,
    in «THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH»,
    vol. 13,
    2000
    , pp. 305 -
    338
  2. V. Hartonas-Garmhausen; E.M. Clarke; S. Campos; Alessandro Cimatti; Fausto Giunchiglia,
    in «SCIENCE OF COMPUTER PROGRAMMING»,
    vol. 36,
    2000
    , pp. 53 -
    64
  3. Alessandro Cimatti; E.M. Clarke; Fausto Giunchiglia; Marco Roveri,
    NuSMV: a new symbolic model checker,
    in «INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER»,
    2000
    , pp. 410 -
    425
  4. Alessandro Cimatti; Luciano Serafini,
    A Context-Based Mechanization of Multi-Agent Reasoning,
    Formal Aspects of Context,
    Drodecht,
    Kluwer,
    2000
    , pp. 65 -
    83
  5. Piergiorgio Bertoli; Alessandro Cimatti; Paolo Traverso,
    Integrating Formal Methods into the Development Cycle of a Safety-critical Embedded Software System,
    5th International Workshop on Formal Methods for Industrial Critical Systems [FMICS],
    2000
    , (5th International Workshop on Formal Methods for Industrial Critical Systems [FMICS],
    Berlin, Germany,
    2000)
  6. Alessandro Cimatti; Marco Roveri,
    Forward Conformant Planning via Symbolic Model Checking,
    AIPS 2000 Workshop on Model-Theoretic Approaches to Planning,
    2000
    , (AIPS 2000 Workshop on Model-Theoretic Approaches to Planning,
    2000)
  7. Alessandro Cimatti; Marco Roveri,
    Conformant Planning via Model Checking,
    Fifth European Conference on Planning [ECP`99],
    Springer,
    2000
    , pp. 21-
    34
    , (Fifth European Conference on Planning [ECP`99],
    Durham, UK,
    08/09/1999 - 10/09/1999)

1999

  1. Alessandro Cimatti; E.M. Clarke; Fausto Giunchiglia; Marco Roveri,
    NuSMV: a New Symbolic Model Verifier,
    11th International Conference on Computer Aided Verification (CAV`99), Proceedings,
    Springer,
    1999
    , (11th International Conference on Computer Aided Verification (CAV`99), Proceedings,
    Trento, Italy,
    1999)
  2. Alessandro Cimatti; P.L. Pieraccini; Roberto Sebastiani; Paolo Traverso; Adolfo Villafiorita,
    Formal Specification and validation of a Vital Communication Protocol,
    FM`99-Formal Methods, World Congress on Formal methods in the Development of Computing Systems,
    1999
    , pp. 1584-
    1604
    , (FM`99-Formal Methods, World Congress on Formal methods in the Development of Computing Systems,
    1999)
  3. A. Chiappini; Alessandro Cimatti; C. Porzia; G. Rotondo; Roberto Sebastiani; Paolo Traverso; Adolfo Villafiorita,
    18th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1999),
    Springer,
    vol.1698,
    1999
    , pp. 410-
    419
    , (18th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1999),
    Toulouse, France,
    1999)
  4. Alessandro Cimatti; Marco Roveri,
    Conformant Planning via Model Checking,
    Fifth European Conference on Planning [ECP`99],
    Springer,
    1999
    , (Fifth European Conference on Planning [ECP`99],
    Durham, UK,
    08/09/1999 - 10/09/1999)
  5. Alessandro Cimatti; Fausto Giunchiglia; Paolo Traverso; Adolfo Villafiorita,
    FLoC`99 Workshop on Run-Time Result Verification,
    1999
    , (FLoC`99 Workshop on Run-Time Result Verification,
    Trento, Italy,
    1999)

1998

  1. Alessandro Cimatti; Fausto Giunchiglia; R.W. Weyhrauch,
    A Many Sorted Natural Deduction,
    in «COMPUTATIONAL INTELLIGENCE»,
    vol. 1,
    n. 14,
    1998
    , pp. 135 -
    150
  2. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; D. Romano; F. Torielli; Paolo Traverso,
    in «FORMAL ASPECTS OF COMPUTING»,
    1998
    , pp. 361 -
    380
  3. Alessandro Cimatti; E.M. Clarke; Fausto Giunchiglia; Marco Roveri,
    NuSMV: A Reimplementation of SMV,
    International Workshop on Software Tools for Technology Transfer (STTT-98),
    vol.NS-98-4,
    1998
    , pp. 25-
    31
    , (International Workshop on Software Tools for Technology Transfer (STTT-98),
    1998)
  4. Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Fourth International Conference on Artificial Intelligence Planning Systems [AIPS-98],
    1998
    , (Fourth International Conference on Artificial Intelligence Planning Systems [AIPS-98],
    Pittsburgh, USA,
    1998)
  5. Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains,
    Fifteenth National Conference on Artificial Intelligence [AAAI 98],
    AAAI Press,
    1998
    , pp. 875-
    881
    , (Fifteenth National Conference on Artificial Intelligence [AAAI 98],
    Madison, USA,
    1998)
  6. Piergiorgio Bertoli; Alessandro Cimatti; Fausto Giunchiglia; Paolo Traverso,
    A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools,
    17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Springer,
    vol.1516,
    1998
    , pp. 221-
    230
    , (17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Heidelberg, Germany,
    1998)
  7. Alessandro Cimatti; Fausto Giunchiglia; Marco Roveri,
    Abstraction in Planning via Model Checking,
    Symposium on Abstraction, Reformulation and Approximation (SARA 1998),
    1998
    , pp. 37-
    41
    , (Symposium on Abstraction, Reformulation and Approximation (SARA 1998),
    1998)
  8. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; D. Romano; F. Torielli; Paolo Traverso,
    Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System,
    17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Springer,
    vol.1516,
    1998
    , pp. 284-
    295
    , (17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Heidelberg, Germany,
    1998)
  9. Alessandro Cimatti; Roberto Sebastiani,
    Servizi forniti dagli strati Safety Layer e Connection Manager,
    Obiettivo del presente documento è fornire una (proposta preliminare di) descrizione dei servizi forniti agli applicativi dagli strati Connection Manager (CM) e Safety Layer (SL), come perzialmente descritto nei documenti (1) e (3). Tale proposta è risultante della riunione in Ansaldo del 08-05-98 tra Ansaldo e Irst,
    1998
  10. Alessandro Cimatti; Roberto Sebastiani,
    Specifica formale dei protocolli Safety Layer e Connection Manager,
    Il presente documento descrive una specifica formale del protocollo di comunicazione tra applicativi in sicurezza basato su ridondanza. Il protocollo è stato suddiviso in due livelli separati, il Safety Layer (SL), come parzialmente descritto nei documenti (1) e (3), ed il Connection Manager (CM). Il S: e il CM sono stati specificati formalmente in SDL, e sono state applicate tecniche di validazione basate su simulazione esaustiva (model checking) attraverso il tool ObjectGEODE Nel presente documento vengono descritti i servizi forniti da tali livelli, e viene descritta la specifica formale delle macchine a stati che realizzano i livelli CM e SL. i dettagli del codice SDL sono descritti nel documento (6).,
    1998
  11. Alessandro Cimatti; Roberto Sebastiani,
    Protocolli Safety Layer e Connection Manager: Descrizione del Codice SDL,
    Nel presente documento viene descritto in dettaglio il codice SDL della specifica formale dei protocolli Safety Layer (SL) e Connection Manager (CM) descritta in (1). Il modello è realizzato attraverso i meccanismi di 'definizione di tipo' e di 'istanziazione' di SDL. Il codice è ripartito nei fine terminale_lib.pr, contenente la descrizione dei tipi (es. macchina SL, macchina CM), e Modello.pr, contentenente le istanze che realizzano la particolare configurazione analizzata Il presente documento assume che il lettore abbia una certa conoscenza di SDL, e fa esplicito riferimento al listato dei file Modello.pr e terminale_lib.pr allegato.,
    1998

1997

  1. Alessandro Cimatti; Enrico Giunchiglia; Fausto Giunchiglia; Paolo Traverso,
    4th European Conference on Planning [ECP`97],
    Springer,
    vol.1348,
    1997
    , pp. 130-
    142
    , (4th European Conference on Planning [ECP`97],
    Toulouse, France,
    1997)
  2. Alessandro Cimatti; Fausto Giunchiglia; P. Pecchiari; B. Pietra; J. Profeta; D. Romano; Paolo Traverso; B. Yu,
    A Provably Correct Embedded Verifier for the Certification of Safety Critical Software,
    Computer Aided Verification - 9th International Conference (CAV 1997),
    Springer,
    vol.1254,
    1997
    , pp. 202-
    213
    , (Computer Aided Verification - 9th International Conference (CAV 1997),
    Haifa, Israel,
    1997)
  3. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; D. Romano; F. Torielli; Paolo Traverso,
    Third International SPIN Workshop [SPIN97],
    1997
    , (Third International SPIN Workshop [SPIN97],
    1997)
  4. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; B. Pietra; D. Romano; F. Torielli; Paolo Traverso,
    Formal Validation & Verification of Software for Railway Control and Protection Systems: Experimental Applications in ANSALDO,
    World Congress on Railway Research [WCRR`97],
    1997
    , pp. 467-
    473
    , (World Congress on Railway Research [WCRR`97],
    Florence, Italy,
    1997)
  5. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; B. Pietra; D. Romano; F. Torielli; Paolo Traverso,
    Formal Validation of an Interlocking System for Large Railway Stations: A Case Study,
    The goal of this document is to define a case study in formal verification, based on a complex real-world application developed by Ansaldo Trasporti. The application, called ACC, is a highly programmable and scalable interlocking system for the control of large railway stations. In the case study, several features of the ACC are omitted in order to limit the complexity. However, the case study still retains a close similarity to the architecture of the ACC, and raises a number of problems of interest for the problem of the formal validation of the real system,
    1997
  6. Alessandro Cimatti; Enrico Giunchiglia; Fausto Giunchiglia; Paolo Traverso,
    A Model Based Decision Procedure for Common Sense Temporal Reasoning,
    In this paper we propose a model based decision procedure for common sense temporal reasoning. This procedure exploits and enhances Lifschitz` work and distinction between action language and query language and Clarke`s work on symbolic model checking. In particular, it allows us to retain the full xpressibility of the temporal formalism and, at the same time, to perform efficient reasoning and to scale up to very complex problems, comparable or more complex than those dealt with by the current state-of-the-art planners,
    1997
  7. Piergiorgio Bertoli; Alessandro Cimatti; Fausto Giunchiglia; Paolo Traverso,
    Certification of Translators via Off-line and On-line Proof Logging and Checking,
    Using non failure-safe components in the implementation of safety-critical systems is desirable because of the extremely high cost of certified components. In order to enhance the safety of such systems, we adopt a solution based on the idea of verifying each single execution of the software running upon them. In particular, we consider the class of translation-based tools used in the development of safety-critical systems. In order to perform the verification in an automatic and efficient way, we follow an innovative approach, by distinguishing an off-line and an on-line verification phases. Each proof in the two phases is guaranteed correct thanks to the use of a logging-and-checking architecture for the tools used to generate them. We describe in detail the off-line and on-line logging-and-checking methodology, its application in the frame of an industrial project, and the ongoing logging-and-checking redesign of a state-of-the-art prover which we intend to use in future applications,
    1997

1996

  1. Alessandro Cimatti; Paolo Traverso,
    Computational Reflection via Mechanized Logical Deduction,
    in «INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS»,
    vol. 11,
    n. 5,
    1996
    , pp. 279 -
    293
  2. Enrico Giunchiglia; Alessandro Armando; Paolo Traverso; Alessandro Cimatti,
    Visual Representation of Natural Language Scene Descriptions,
    in «IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS»,
    vol. 26,
    n. 8,
    1996
    , pp. 279 -
    293
  3. Paolo Bouquet; Alessandro Cimatti,
    Mechanizing Local Reasoning with Contexts,
    Working notes of the IJCAI-95 Workshop on ``Modelling Context in Knowledge Representation and Reasoning``,
    1996
    , pp. 13-
    23
    , (Working notes of the IJCAI-95 Workshop on ``Modelling Context in Knowledge Representation and Reasoning``,
    Montreal, Canada,
    1995)
  4. Alessandro Cimatti; Luciano Serafini,
    Mechanizing Multi-Agent Reasoning with Belief Contexts,
    Practical Reasoning, International Conference on Formal and Applied Practical Reasoning [FAPR`96],
    Springer,
    1996
    , pp. 694-
    696
    , (Practical Reasoning, International Conference on Formal and Applied Practical Reasoning [FAPR`96],
    1996)
  5. Massimo Benerecetti; Alessandro Cimatti; Enrico Giunchiglia; Fausto Giunchiglia; Luciano Serafini,
    Context-Based Formal Specification of Multi-Agent Systems,
    Working Notes of the Third International Workshop on Agent Theories, Architectures, and Languages [ATAL-96],
    1996
    , pp. 295-
    307
    , (Working Notes of the Third International Workshop on Agent Theories, Architectures, and Languages [ATAL-96],
    Budapest, Hungary,
    1996)

1995

  1. A. Armando; Alessandro Cimatti; E. Giunchiglia; P. Pecchiari; L. Spalazzi; Paolo Traverso,
    Flexible Planning by Integrating Multilevel Reasoning,
    in «ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE»,
    vol. 4,
    1995
    , pp. 401 -
    412
  2. Giuliano Antoniol; Bruno Caprile; Alessandro Cimatti; Roberto Fiutem,
    Experiencing Real-Life Interactions with the Mobile Platform of MAIA,
    The Biology and Technology of Intelligent Autonomous Agents: Proceedings of the NATO Advanced Study on the Biology and Technology of Intelligent Autonomous Agents,
    Springer,
    1995
    , pp. 296-
    311
    , (The Biology and Technology of Intelligent Autonomous Agents: Proceedings of the NATO Advanced Study on the Biology and Technology of Intelligent Autonomous Agents,
    1993)
  3. Alessandro Cimatti; Luciano Serafini,
    Multi-Agent Reasoning with Belief Contexts III: Towards the Mechanization,
    IJCAI-95 Workshop on Modelling Context in Knowledge Representation and Reasoning,
    1995
    , pp. 35-
    45
    , (IJCAI-95 Workshop on Modelling Context in Knowledge Representation and Reasoning,
    Montreal, Canada,
    1995)
  4. Alessandro Cimatti; Luciano Serafini,
    Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study,
    Intelligent Agents, ECAI-94 Workshop on Agent Theories, Architectures, and Languages,
    Springer,
    vol.890,
    1995
    , pp. 71-
    85
    , (Intelligent Agents, ECAI-94 Workshop on Agent Theories, Architectures, and Languages,
    Amsterdam, The Netherlands,
    1994)
  5. Alessandro Cimatti; Luciano Serafini,
    Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance,
    First International Conference on Multiagent Systems,
    MIT Press,
    1995
    , pp. 57-
    64
    , (First International Conference on Multiagent Systems,
    San Francisco, California,
    1995)

1994

  1. Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Enrico Giunchiglia; Alessandro Armando,
    MRG: Building planners for real world complex applications,
    in «APPLIED ARTIFICIAL INTELLIGENCE»,
    1994
    , pp. 333 -
    357
  2. Fausto Giunchiglia; Alessandro Armando; Alessandro Cimatti; Paolo Traverso,
    First steps towards provably correct system synthesis of system code,
    CADE-12 Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems,
    1994
    , pp. 28-
    30
    , (CADE-12 Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems,
    Nancy, France,
    1994)

1993

  1. Fausto Giunchiglia; Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Sandro Dalbosco; Luciano Serafini; Enrico Giunchiglia; Alessandro Armando; Paolo Pecchiari,
    MRG: sistema di ragionamento,
    in «AUTOMAZIONE E STRUMENTAZIONE»,
    vol. 9,
    1993
    , pp. 97 -
    103
  2. Fausto Giunchiglia; Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Sandro Dalbosco; Luciano Serafini; Enrico Giunchiglia; Alessandro Armando; Paolo Pecchiari,
    MRG: un nucleo di ragionamento per un sistema integrato multifunzionale,
    in «SISTEMI INTELLIGENTI»,
    vol. 3,
    1993
    , pp. 435 -
    460
  3. Paolo Traverso; Luca Spalazzi; Alessandro Cimatti,
    A planning language and a semantics for real world autonomous agents,
    1993 Italian Planning Workshop,
    1993
    , (1993 Italian Planning Workshop,
    Roma, Italy,
    1993)
  4. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; D. Romano; F. Torielli; Paolo Traverso,
    Valutazione del CBR-tool orientato all`help desk `Case Advisor`,
    In questo documento ci prefiggiamo di riportare gli esiti della valutazione di CaseAdvisor, strumento sviluppato dalla ICue Technology Inc., per il supporto del problem solving interattivo basato sul Case-Based Reasoning (CBR). Il gruppo fa capo a Qiang Yang, direttore dell`Information Service Agents Lab (ISA Lab) presso la Simon Fraser University (Burnaby, BC, Canada). Il prodotto in oggetto è stato inizialmente sviluppato per l`ambiente Windows, mentre una seconda versione in Java è attualmente in fase di sviluppo. A fini di valutazione, ci sono state fornite una versione `demo` per Windows ed un prototipo dell`applicazione in Java. La suite di tool per WIndows conmprende tre moduli: uno per la memorizzazione dei case-base su database relazionali, uno per l`authoring ed il mantenimento dei casi, ed un terzo per l`impiego della conoscenza presente nel CB e mirato alle applicazioni `Help Desk`. Nel presente documento ci occuperemo in dettaglio dei tre moduli, e passeremo rapidamente in rassegna le caratteristiche del prototipo in Java,
    1993

1992

  1. Paolo Traverso; Alessandro Cimatti; Luca Spalazzi,
    Beyond the single planning paradigm: introspective planning,
    10th European Conference on Artificial Intelligence (ECAI 1992),
    Wiley,
    1992
    , pp. 643-
    647
    , (10th European Conference on Artificial Intelligence (ECAI 1992),
    Vienna, Austria,
    1992)
  2. Luca Spalazzi; Alessandro Cimatti; Paolo Traverso,
    Implementing planning as tactical reasoning,
    3rd Annual Conference on Artificial Intelligence, Simulation & Planning in High Autonomy Systems (AIS`92),
    IEEE Computer Society,
    1992
    , pp. 80-
    85
    , (3rd Annual Conference on Artificial Intelligence, Simulation & Planning in High Autonomy Systems (AIS`92),
    Perth, Western Australia,
    1992)
  3. Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Enrico Giunchiglia,
    Building planners with explicit control mechanism,
    2nd International Symposium on Artificial Intelligence and Mathematics (ISAI 1992),
    AAAI Press,
    1992
    , pp. 195-
    202
    , (2nd International Symposium on Artificial Intelligence and Mathematics (ISAI 1992),
    Cancun, Mexico,
    1992)
  4. Alessandro Cimatti; Paolo Traverso; Luca Spalazzi,
    Programming Planners with Flexible Architectures,
    AI and Cognitive Science `92,
    Springer Verlag,
    1992
    , pp. 311-
    314
    , (AI and Cognitive Science `92,
    Limerick, Ireland,
    1992)
  5. Alessandro Cimatti; Paolo Traverso; Sandro Dalbosco; Alessandro Armando,
    Navigation by Combining Reactivity and Planning,
    Intelligent Vechicles `92 Symposium,
    IEEE Industrial Electronics,
    1992
    , pp. 265-
    270
    , (Intelligent Vechicles `92 Symposium,
    Detroit, USA,
    1992)
  6. Fausto Giunchiglia; Paolo Traverso; Alessandro Cimatti; Paolo Pecchiari,
    A System for Multi-Level Reasoning,
    IMSA `92, International Workshop on New Models for Software Architecture,
    1992
    , pp. 190-
    195
    , (IMSA `92, International Workshop on New Models for Software Architecture,
    Tokyo, Japan,
    1992)
  7. Fausto Giunchiglia; Paolo Traverso; Alessandro Cimatti; Luca Spalazzi,
    Tactics: extending the notion of plan,
    ECAI-92 Workshop `Beyond Sequential Planning`,
    1992
    , (ECAI-92 Workshop `Beyond Sequential Planning`,
    Vienna, Austria,
    1992)
  8. Fausto Giunchiglia; Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Sandro Dalbosco; Luciano Serafini; Enrico Giunchiglia; Alessandro Armando; Paolo Pecchiari,
    Un nucleo di ragionamento per un sistema integrato multi-funzionale: stato di avanzamento,
    Automation 1992, 36th ANIPLA Conference,
    Pirella,
    1992
    , pp. 620-
    633
    , (Automation 1992, 36th ANIPLA Conference,
    Genova,
    1992)
  9. Fausto Giunchiglia; Alessandro Cimatti; Sandro Dalbosco; Paolo Traverso; Luca Spalazzi,
    MRG: un sistema di ragionamento distribuito per applicazioni complesse,
    Atti seconda giornata di lavoro del gruppo Intelligenza Artificiale Distribuita (DAI) dell`AI*IA,
    1992
    , (Atti seconda giornata di lavoro del gruppo Intelligenza Artificiale Distribuita (DAI) dell`AI*IA,
    Roma,
    1992)

DBLP

Research Gate