Alessandro Cimatti

Researcher and Director of DI Center

    Publications

    1. Panjkovic, Stefan; Micheli, Andrea; Cimatti, Alessandro,
      Deciding Unsolvability in Temporal Planning under Action Non-Self-Overlapping,
      Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI2022,
      2022
    2. Bittner, Benjamin; Bozzano, Marco; Cimatti, Alessandro; Gario, Marco Elio Gustavo; Tonetta, Stefano; Vozárová, Viktória,
      Diagnosability of fair transition systems,
      in «ARTIFICIAL INTELLIGENCE»,
      vol. 309,
      2022
    3. Tierno, A.; Turri, G.; Cimatti, A.; Passerone, R.,
      Automatic Design Space Exploration of Redundant Architectures,
      Proceedings of International Conference on Applications in Electronics Pervading Industry, Environment and Society,
      vol. 866,
      2022
      , pp. 149-
      159
    4. Bozzano, Marco; Cimatti, Alessandro; Gario, Marco Elio Gustavo; Jones, David; Mattarei, Cristian,
      Model-based Safety Assessment of a Triple Modular Generator with XSAP,
      in «FORMAL ASPECTS OF COMPUTING»,
      vol. 33,
      n. 2,
      2021
      , pp. 251-
      295
    5. Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca,
      Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning,
      28th International Conference on Automated Deduction, Proceedings,
      vol. 12699,
      2021
      , pp. 131-
      147
    6. Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico,
      Proving the Existence of Fair Paths in Infinite-State Systems,
      Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021,
      vol. 12597,
      2021
      , pp. 104-
      126
    7. Bozzano, Marco; Cimatti, Alessandro; Fernandes Pires, Anthony; Griggio, Alberto; Jonas, Martin; Kimberly, Greg,
      Efficient SMT-Based Analysis of Failure Propagation,
      Proceedings of Computer Aided Verification - 33rd International Conference, (CAV2021), Virtual Event, Part II,
      Springer,
      vol. 12760,
      2021
      , pp. 209-
      230
    8. Bozzano, Marco; Cimatti, Alessandro; Roveri, Marco,
      A Comprehensive Approach to On-board Autonomy Verification and Validation,
      in «ACM TRANSACTIONS ON INTELLIGENT SYSTEMS AND TECHNOLOGY»,
      vol. 12,
      n. 4,
      2021
      , pp. 1-
      29
    9. Cimatti, Alessandro; Tian, Chun; Tonetta, Stefano,
      Assumption-Based Runtime Verification of Infinite-State Systems,
      Proceedings of Runtime Verification (RV 2021),
      vol. 12974,
      n. 11,
      2021
      , pp. 207-
      227
    10. Cimatti, Alessandro; Geatti, Luca; Gigante, Nicola; Montanari, Angelo; Tonetta, Stefano,
      Extended bounded response LTL: a new safety fragment for efficient reactive synthesis,
      in «FORMAL METHODS IN SYSTEM DESIGN»,
      2021
    11. Cimatti, Alessandro; Geatti, Luca; Gigante, Nicola; Montanari, Angelo; Tonetta, Stefano,
      Expressiveness of Extended Bounded Response LTL,
      in «ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE»,
      ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE,
      vol. 346,
      2021
      , pp. 152-
      165
    12. Syifa'ul Mufid, Muhammad; Micheli, Andrea; Abate, Alessandro; Cimatti, Alessandro,
      SMT-Based Model Checking of Max-Plus Linear Systems,
      32nd International Conference on Concurrency Theory (CONCUR 2021),
      2021
    13. Cashmore, Michael; Cimatti, Alessandro; Magazzeni, Daniele; Micheli, Andrea; Zehtabi, Parisa,
      Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans,
      Proceedings of 13:1--13:128th International Symposium on Temporal Representation and Reasoning (TIME 2021),
      Schloss Dagstuhl -- Leibniz-Zentrum fur Informatik,
      2021
      , pp. 13:1-
      13:14
    14. Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano,
      Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems,
      Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, Proceedings, Part I,
      Springer,
      vol. 12759,
      2021
      , pp. 529-
      551
    15. Cimatti, Alessandro; Geatti, Luca; Gigante, Nicola; Montanari, Angelo; Tonetta, Stefano,
      Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis,
      Proceedings of Software Engineering and Formal Methods - 19th International Conference,SEFM 2021,
      Springer,
      vol. 13085,
      2021
      , pp. 351-
      371
    16. Bartali, Ruben; Christodoulaki, Rosie; Drosou, Vassiliki; Baker Derek, Keith; Svaizer, Piergiorgio; Alarcón-Padilla, Diego-César; Osório, Tiago; Kramer, Wolfgang; Bolognese, Michele; Pratticò, Luca; Viesi, Diego; Roca Sobrino, Lidia; Guillen Burrieza, Elena; Fluch, Juergen; Bayer, Özgür; Pınarlı, Deniz; Erdoğan, Selin; Brunner, Christoph; Cavada, Roberto; Bonizzi, Alberto; Cimatti, Alessandro; Zanetti, Alberto; Crema, Luigi,
      Decarbonization of industrial processes: technologies, applications and perspectives of low-temperature solar heat (80-150°C),
      EuroSun 2020 Proceedings,
      2021
      , pp. 1-
      13
    17. Becchi, Anna; Cimatti, Alessandro; Zaffanella, Enea,
      Reverse engineering with P-stable Abstractions,
      Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the Twelfth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021), Padua, Italy, September 22, 2021,
      vol. 2987,
      2021
      , pp. 91-
      95
    18. Bigarella, Filippo; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Jonáš, Martin; Roveri, Marco; Sebastiani, Roberto; Trentin, Patrick,
      Optimization Modulo Non-linear Arithmetic via Incremental Linearization,
      Frontiers of Combining Systems 13th International Symposium, FroCoS 2021,
      vol. 12941,
      2021
      , pp. 213-
      231
    19. Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico; Roveri, Marco; Tonetta, Stefano,
      SMT-Based Satisfiability of First-Order LTL with Event Freezing Functions and Metric Operators,
      in «INFORMATION AND COMPUTATION»,
      vol. 272,
      2020
    20. Valentini, Alessandro; Micheli, Andrea; Cimatti, Alessandro,
      Temporal Planning with Intermediate Conditions and Effects,
      Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI-20),
      AAAI Press,
      vol. 34,
      n. 6,
      2020
    21. Cimatti, Alessandro; Geatti, Luca; Gigante, Nicola; Montanari, Angelo; Tonetta, Stefano,
      Reactive Synthesis from Extended Bounded Response LTL Specifications,
      Proceedings of the 20th International Conference on Formal Methods in Computer-Aided Design (FMCAD),
      2020
    22. Cimatti, Alessandro; Geatti, Luca; Griggio, Alberto; Kimberly, Greg; Tonetta, Stefano,
      Safe Decomposition of Startup Requirements: Verification and Synthesis,
      Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, (TACAS) 2020, Held as Part of theEuropean Joint Conferences on Theory and Practice of Software, (ETAPS) 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part (I),
      Springer,
      vol. 12078,
      2020
      , pp. 155-
      172
    23. Abate, Alessandro; Cimatti, Alessandro; Micheli, Andrea; Mufid, Muhammad Syifa’ul,
      Computation of the Transient in Max-Plus Linear Systems via SMT-Solving,
      Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Vienna, Austria, September 1-3, 2020, Proceedings,
      vol. 12288,
      2020
      , pp. 161-
      177
    24. Beirami, H.; Calzà, D.; Cimatti, A.; Islam, M. M.; Roveri, M.; Svaizer, P.,
      Predicting RUL of Bearings in the Pumps of a Critical Industrial Air Treatment System,
      Proceedings of the 5th European Conference of the Prognostics and Health Management Society 2020,
      PHM Society,
      vol. 5,
      n. 1,
      2020
      , pp. 12-
      22
    25. Beirami, H.; Calzà, D.; Cimatti, A.; Islam, M.; Roveri, M.; Svaizer, P.,
      A Data-driven Approach for RUL Prediction of an Experimental Filtration System,
      Proceedings of the 5th European Conference of the Prognostics and Health Management Society 2020,
      PHM Society,
      vol. 5,
      n. 1,
      2020
    26. Amendola, Arturo; Becchi, Anna; Cavada, Roberto; Cimatti, Alessandro; Griggio, Alberto; Scaglione, Giuseppe; Susi, Angelo; Tacchella, Alberto; Tessi, Matteo,
      A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System,
      Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020,
      Springer,
      vol. 12478,
      2020
      , pp. 240-
      254
    27. Becchi, Anna; Cimatti, Alessandro; Zaffanella, Enea,
      Synthesis of P-Stable Abstractions,
      Proceedings of Software Engineering and Formal Methods - 18th International Conference, SEFM 2020,
      vol. 12310,
      2020
      , pp. 214-
      230
    28. Bozzano, M.; Cimatti, A.; Mattarei, C.,
      Formal reliability analysis of redundant architectures,
      in «FORMAL ASPECTS OF COMPUTING»,
      vol. 31,
      n. 1,
      2019
      , pp. 59-
      94
    29. Bozzano, Marco; Bruintjes, Harold; Cimatti, Alessandro; Katoen, Joost-Pieter; Noll, Thomas; Tonetta, Stefano,
      COMPASS 3.0,
      Tools and Algorithms for the Construction and Analysis of Systems,
      Springer,
      vol. 11427,
      2019
      , pp. 379-
      385
    30. Cashmore, Michael; Cimatti, Alessandro; Magazzeni, Daniele; Micheli, Andrea; Zehtabi, Parisa,
      Robustness Envelopes for Temporal Plans,
      Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-19),
      vol. 33,
      2019
    31. Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico; Roveri, Marco; Tonetta, Stefano,
      Extending nuXmv with Timed Transition Systems and Timed Temporal Properties,
      Proceedings of Computer Aided Verification - 31st International Conference, CAV 2019,
      vol. 11561,
      2019
      , pp. 376-
      386
    32. Cimatti, Alessandro; Delong, Rance; Stojic, Ivan; Tonetta, Stefano,
      Model-Based Run-Time Synthesis of Architectural Configurations for Adaptive MILS Systems,
      Computer Safety, Reliability, and Security - Proceedings of the 38th International Conference,SAFECOMP 2019,
      Springer,
      vol. 11698,
      2019
      , pp. 200-
      215
    33. Cimatti, Alessandro; Tian, Chun; Tonetta, Stefano,
      Assumption-based Runtime Verification with Partial Observability and Resets,
      Runtime Verification (RV 2019),
      Springer,
      vol. 11757,
      n. 10,
      2019
      , pp. 165-
      184
    34. Cimatti, Alessandro; Tian, Chun; Tonetta, Stefano,
      NuRV: a nuXmv Extension for Runtime Verification,
      Runtime Verification (RV 2019),
      Springer,
      vol. 11757,
      n. 23,
      2019
      , pp. 382-
      392
    35. Cimatti, Alessandro; Do, Minh; Micheli, Andrea; Roveri, Marco; Smith, David E.,
      Strong temporal planning with uncontrollable durations,
      in «ARTIFICIAL INTELLIGENCE»,
      vol. 256,
      2018
      , pp. 1-
      34
    36. Cimatti, Alessandro; Demasi, Ramiro Adrian; Tonetta, Stefano,
      Tightening the contract refinements of a system architecture,
      in «FORMAL METHODS IN SYSTEM DESIGN»,
      vol. 52,
      n. 1,
      2018
      , pp. 88-
      116
    37. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto,
      Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization,
      Proceedings of Theory and Applications of Satisfiability Testing – SAT 2018,
      vol. 10929,
      2018
      , pp. 383-
      398
    38. Cimatti, Alessandro; Stojic, Ivan; Tonetta, Stefano,
      Formal Specification and Verification of Dynamic Parametrized Architectures,
      Formal Methods - 22nd International Symposium, FM 2018, Held asPart of the Federated Logic Conference, FloC 2018, Proceedings,
      Springer,
      vol. 10951,
      2018
      , pp. 625-
      644
    39. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto,
      Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions,
      in «ACM TRANSACTIONS ON COMPUTATIONAL LOGIC»,
      vol. 19,
      n. 3,
      2018
      , pp. 1-
      52
    40. Cavada, Roberto; Cimatti, Alessandro; Mover, Sergio; Sessa, Mirko; Cadavero, Giuseppe; Scaglione, Giuseppe,
      Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks,
      Proceedings of 2018 Formal Methods in Computer Aided Design, FMCAD 2018,
      2018
    41. Cimatti, Alessandro; Ghilardi, Silvio; Ranise, Silvio,
      Model checking: teoria ed applicazioni,
      Le direzioni della ricerca logica in Italia 2,
      Edizioni ETS,
      2018
      , pp. 141-
      193
    42. Mechtaev, Sergey; Griggio, Alberto; Cimatti, Alessandro; Roychoudhury, Abhik,
      Symbolic execution with existential second-order constraints,
      Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018,
      2018
      , pp. 389-
      399
    43. Cimatti, Alessandro; Delong, Rance; Stojic, Ivan; Tonetta, Stefano,
      Towards Adaptive MILS Systems: Model-Based Design, Verification And Run-Time Adaptation,
      2018
    44. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto,
      Incremental Linearization: A practical approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions,
      Proceedings of 2018 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing,
      2018
    45. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto,
      Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF,
      Tools and Algorithms for the Construction and Analysis of Systems,
      vol. 10205,
      2017
      , pp. 58-
      75
    46. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto,
      Satisfiability Modulo Transcendental Functions via Incremental Linearization,
      Automated Deduction – CADE 26,
      vol. 10395,
      2017
      , pp. 95-
      113
    47. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco,
      Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic,
      Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence,
      AAAI Press,
      2017
      , pp. 3547-
      3554
    48. Cimatti, Alessandro; Mover, Sergio; Sessa, Mirko,
      SMT-based analysis of switching multi-domain linear Kirchhoff networks,
      Proceedings of Formal Methods in Computer Aided Design (FMCAD 2017),
      2017
      , pp. 188-
      195
    49. Bittner, Benjamin; Bozzano, Marco; Cimatti, Alessandro,
      Timed Failure Propagation Analysis for Spacecraft Engineering: The ESA Solar Orbiter Case Study,
      Proceedings of International Symposium on Model-Based Safety and Assessment,
      Springer,
      vol. 10437,
      2017
      , pp. 255-
      271
    50. Bozzano, Marco; Bruintjes, Harold; Cimatti, Alessandro; Katoen, Joost-Pieter; Noll, Thomas; Tonetta, Stefano,
      Formal Methods for Aerospace Systems,
      Cyber-Physical System Design from an Architecture Analysis Viewpoint,
      Springer,
      2017
      , pp. 133-
      159
    51. Bittner, Benjamin; Bozzano, Marco; Cavada, Roberto; Cimatti, Alessandro; Gario, Marco Elio Gustavo; Griggio, Alberto; Mattarei, Cristian; Micheli, Andrea; Zampedri, Gianni,
      The xSAP Safety Analysis Platform,
      Tools and Algorithms for the Construction and Analysis of Systems,
      Springer Berlin Heidelberg,
      vol. 9636,
      2016
      , pp. 533-
      539
    52. Cimatti, Alessandro; Hunsberger, Luke; Micheli, Andrea; Posenato, Roberto; Roveri, Marco,
      Dynamic controllability via Timed Game Automata,
      in «ACTA INFORMATICA»,
      2016
      , pp. 1-
      42
    53. Bittner, Benjamin; Bozzano, Marco; Cimatti, Alessandro; Zampedri, Gianni,
      Automated Verification and Tightening of Failure Propagation Models,
      Proceedings of the 30th AAAI Conference on Artificial Intelligence (AAAI 2016),
      2016
      , pp. 907-
      913
    54. Bittner, Benjamin; Bozzano, Marco; Cimatti, Alessandro,
      Automated Synthesis of Timed Failure Propagation Graphs,
      Proceedings of the 25th International Joint Conference on Artificial Intelligence, IJCAI,
      2016
      , pp. 972-
      978
    55. Ábrahám, Erika; Abbott, John; Becker, Bernd; Bigatti, Anna M.; Brain, Martin; Buchberger, Bruno; Cimatti, Alessandro; Davenport, James H.; England, Matthew; Fontaine, Pascal; Forrest, Stephen; Griggio, Alberto; Kroening, Daniel; Seiler, Werner M.; Sturm, Thomas,
      SC^2: Satisfiability Checking Meets Symbolic Computation,
      Intelligent Computer Mathematics - 9th International Conference, CICM 2016,
      vol. 9791,
      2016
      , pp. 28-
      43
    56. Jakub, Daniel; Cimatti, Alessandro; Griggio, Alberto; Tonetta, Stefano; Mover, Sergio,
      Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations,
      Computer Aided Verification - 28th International Conference, CAV 2016,
      vol. 9779,
      2016
      , pp. 271-
      291
    57. Irfan, Ahmed; Cimatti, Alessandro; Griggio, Alberto; Roveri, Marco; Sebastiani, Roberto,
      Verilog2SMV: A Tool for Word-level Verification,
      Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016,
      2016
      , pp. 1156-
      1159
    58. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco,
      Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies,
      Proceedings of the Thirtieth AAAI}Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA,
      2016
      , pp. 3116-
      3122
    59. Gario, Marco Elio Gustavo; Cimatti, Alessandro; Mattarei, Cristian; Tonetta, Stefano; Rozier, Kristin Yvonne,
      Model Checking at Scale: Automated Air Traffic Control Design Space Exploration,
      Computer Aided Verification - 28th International Conference CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II,
      vol. 9780,
      2016
      , pp. 3-
      22
    60. Cimatti, Alessandro; Gario, Marco Elio Gustavo; Tonetta, Stefano,
      A Lazy Approach to Temporal Epistemic Logic Model Checking,
      Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems,
      International Foundation for Autonomous Agents and Multiagent Systems,
      2016
      , pp. 1218-
      1226
    61. Cimatti, Alessandro; Demasi, Ramiro Adrian; Tonetta, Stefano,
      Tightening a Contract Refinement,
      Software Engineering and Formal Methods - 14th International Conference,SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8,2016, Proceedings,
      Springer,
      vol. 9763,
      2016
      , pp. 386-
      402
    62. Cimatti, Alessandro; Mover, S.; Sessa, Mirko,
      From Electrical Switched Networks to Hybrid Automata,
      Proceedings of the 21st International Symposium on Formal Methods, FM 2016,
      vol. 9995,
      2016
      , pp. 164-
      181
    63. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      Infinite-state invariant checking with IC3 and predicate abstraction,
      in «FORMAL METHODS IN SYSTEM DESIGN»,
      2016
    64. Cavada, Roberto; Cimatti, Alessandro; Crema, Luigi; Roccabruna, Mattia; Tonetta, Stefano,
      Model-Based Design of an Energy-System Embedded Controller Using Taste,
      Proceedings of FM 2016: Formal Methods 21st International Symposium,
      vol. 9995,
      2016
      , pp. 741-
      747
    65. Ábrahám, E.; Fontaine, P.; Forrest, S.; Griggio, A.; Kroening, D.; Seiler, W. M.; Sturm, T.; Abbott, J.; Becker, B.; Bigatti, A. M.; Brain, M.; Buchberger, B.; Cimatti, A.; Davenport, J. H.; England, M.,
      Satisfiability checking and symbolic computation,
      in «ACM COMMUNICATIONS IN COMPUTER ALGEBRA»,
      vol. 50,
      n. 4,
      2016
      , pp. 145-
      147
    66. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco,
      Solving strong controllability of temporal problems with uncertainty using SMT,
      in «CONSTRAINTS»,
      vol. 20,
      2015
      , pp. 7-
      29
    67. A. Cimatti; S. Tonetta,
      Contracts-refinement proof system for component-based embedded systems,
      in «SCIENCE OF COMPUTER PROGRAMMING»,
      2015
    68. Bozzano, Marco; Cimatti, Alessandro; Oleg, Lisagor; Mattarei, Cristian; Mover, Sergio; Roveri, Marco; Tonetta, Stefano,
      Safety Assessment of AltaRica Models via Symbolic Model Checking,
      in «SCIENCE OF COMPUTER PROGRAMMING»,
      vol. 98,
      2015
      , pp. 464-
      483
    69. Cimatti A.; Micheli A.; Roveri M,
      Strong Temporal Planning with Uncontrollable Durations: a State-Space Approach,
      Proceedings of the 29th AAAI Conference on Artificial Intelligence,
      AAAI Press,
      2015
    70. Bozzano M.; Cimatti A.; Gario M.; Micheli A.,
      SMT-based Validation of Timed Failure Propagation Graphs,
      Proceedings of the 29th AAAI Conference on Artificial Intelligence,
      AAAI Press,
      2015
    71. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      HYCOMP - an SMT-based model checker for hybrid systems,
      Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings,
      Springer,
      vol. 9035,
      2015
      , pp. 52-
      67
    72. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco,
      An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty,
      in «ARTIFICIAL INTELLIGENCE»,
      vol. 224,
      2015
      , pp. 1-
      27
    73. Bozzano, Marco; Cimatti, Alessandro; Gario, Marco Elio Gustavo; Tonetta, Stefano,
      Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic,
      in «LOGICAL METHODS IN COMPUTER SCIENCE»,
      vol. 11,
      n. 4,
      2015
    74. Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano,
      HRELTL: A temporal logic for hybrid systems,
      in «INFORMATION AND COMPUTATION»,
      vol. 245,
      2015
      , pp. 54-
      71
    75. Bozzano, Marco; Cimatti, Alessandro; Griggio, Alberto; Mattarei, Cristian,
      Efficient Anytime Techniques for Model-Based Safety Analysis,
      Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I,
      vol. 9206,
      2015
      , pp. 603-
      621
    76. Mattarei, Cristian; Cimatti, Alessandro; Gario, Marco Elio Gustavo; Tonetta, Stefano; Rozier, Kristin Yvonne,
      Comparing Different Functional Allocations in Automated Air Traffic Control Design,
      Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2015,
      IEEE,
      2015
      , pp. 112-
      119
    77. Bliudze, Simon; Cimatti, Alessandro; Jaber, Mohamad; Mover, Sergio; Roveri, Marco; Saab, Wajeb; Wang, Qiang,
      Formal Verification of Infinite-State BIP Models,
      Proceedings of ATVA,
      Springer,
      vol. 9364,
      2015
      , pp. 326-
      343
    78. Bozzano, Marco; Cimatti, Alessandro; Fernandes Pires, Anthony; Jones, D.; Kimberly, G.; Petri, T.; Robinson, R.; Tonetta, Stefano,
      Formal Design and Safety Analysis of AIR6110 Wheel Brake System,
      Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I,
      vol. 9206,
      2015
      , pp. 518-
      535
    79. Cimatti, Alessandro; Delong, Rance; Marcantonio, Davide; Tonetta, Stefano,
      Combining MILS with Contract-Based Design for Safety and Security Requirements,
      Computer Safety, Reliability, and Security - SAFECOMP 2015 Workshops, ASSURE, DECSoS, ISSE, ReSA4CI, and SASSUR, Delft, The Netherlands, September 22, 2015, Proceedings,
      vol. 9338,
      2015
      , pp. 264-
      276
    80. Bozzano, Marco; Cimatti, Alessandro; Gario, Marco Elio Gustavo; Tonetta, Stefano,
      Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic,
      TACAS 2014, LNCS 8413,,
      Springer-Verlag,
      vol. 8413,
      2014
      , pp. 326-
      340
    81. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano,
      Quantifier-free encoding of invariants for hybrid systems,
      in «FORMAL METHODS IN SYSTEM DESIGN»,
      vol. 45,
      n. 2,
      2014
      , pp. 165-
      188
    82. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      IC3 Modulo Theories via Implicit Predicate Abstraction,
      TACAS,
      Springer,
      vol. 8413,
      2014
      , pp. 46-
      61
    83. Robin Steel;Alexander Hoffmann;Marc Niezette;Alessandro Cimatti;Marco Roveri;Konstantinos Kapellos;Alessandro Donati;Nicola Policella,
      Innovative Rover Operations Concepts - Autonomous Planner (IRONCAP) - Concluding the adventure,
      13th International Conference on Space Operations 2014,
      2014
    84. Bozzano, Marco; Cimatti, Alessandro; Katoen, J. P.; Katsaros, P.; Mokos, K.; Nguyen, V. Y.; Noll, T.; Postma, B.; Roveri, Marco,
      Spacecraft Early Design Validation using Formal Methods,
      in «RELIABILITY ENGINEERING & SYSTEM SAFETY»,
      vol. 132,
      2014
      , pp. 20-
      35
    85. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      Verifying LTL Properties of Hybrid Systems with K-Liveness,
      CAV,
      2014
      , pp. 424-
      440
    86. Cavada, Roberto; Cimatti, Alessandro; Dorigatti, Michele; Griggio, Alberto; Mariotti, Alessandro; Micheli, Andrea; Mover, Sergio; Roveri, Marco; Tonetta, Stefano,
      The nuXmv Symbolic Model Checker,
      CAV,
      2014
      , pp. 334-
      342
    87. Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian; Tonetta, Stefano,
      Formal Safety Assessment via Contract-Based Design.,
      ATVA14,
      2014
      , pp. 81-
      97
    88. Bittner B.; Bozzano M.; Cimatti A.; Gario M.; Griggio A.,
      Towards Pareto-Optimal Parameter Synthesis for Monotonic Cost Functions,
      Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design,
      2014
      , pp. 23-
      30
    89. Cimatti, Alessandro; Hunsberger, L.; Micheli, Andrea; Roveri, Marco,
      Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty,
      Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence,
      AAAI Press,
      2014
      , pp. 2242-
      2249
    90. Cimatti A.; Hunsberger L.; Micheli A.; Posenato R; Roveri M.,
      Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation,
      Proceedings of the 21st International Symposium on Temporal Representation and Reasoning,
      IEEE,
      2014
      , pp. 27-
      36
    91. Guiotto, A.; De Ferluc, R.; Bozzano, Marco; Cimatti, Alessandro; Gario, Marco Elio Gustavo; Yushtein, Y.,
      FAME Process: A Dedicated Development and V&V Process for FDIR,
      ESA SP-725,
      2014
    92. Bittner B.; Bozzano M.; Cimatti A.; De Ferluc R. ; Gario M.; Guiotto A. ; Yushtein Y.,
      An Integrated Process for FDIR Design in Aerospace,
      LNCS 8822,
      Springer International Publishing,
      vol. 8822,
      2014
      , pp. 82-
      95
    93. Bittner, Benjamin; Bozzano, Marco; Cimatti, Alessandro; De Ferluc, R.; Gario, Marco Elio Gustavo; Guiotto, A.; Yushtein, Y.,
      FAME: A Model-Based Environment for FDIR Design in Aerospace,
      Proceedings of the International Symposium on Model Based Safety and Assessment,
      Springer International Publishing,
      vol. 8822,
      2014
      , pp. 1-
      2
    94. Laura Baracchi;Alessandro Cimatti;Gerald Garcia;Silvia Mazzini;Stefano Puri;Stefano Tonetta,
      Requirements Refinement and Component Reuse: The FoReVer Contract-Based Approach,
      Handbook of Research on Embedded Systems Design,
      2014
      , pp. 209-
      241
    95. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano,
      SMT-based scenario verification for hybrid systems,
      in «FORMAL METHODS IN SYSTEM DESIGN»,
      vol. 42,
      n. 1,
      2013
      , pp. 46-
      66
    96. Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian,
      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
    97. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco,
      Software Model Checking SystemC,
      in «IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS»,
      vol. 32,
      2013
      , pp. 774-
      787
    98. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco,
      Timelines with Temporal Uncertainty,
      AAAI,
      David Leake,
      2013
      , pp. 195-
      201
    99. Cimatti, Alessandro; Griggio, Alberto; Bastiaan Joost, Schaafsma; Roberto, Sebastiani,
      The MathSAT5 SMT Solver,
      in «LECTURE NOTES IN ARTIFICIAL INTELLIGENCE»,
      Lecture Notes in Computer ScienceTools and Algorithms for the Construction and Analysis of Systems,
      vol. 7795,
      2013
      , pp. 93-
      107
    100. Cimatti, Alessandro; Griggio, Alberto; Bastiaan Joost, Schaafsma; Roberto, Sebastiani,
      A Modular Approach to MaxSAT Modulo Theories,
      in «LECTURE NOTES IN ARTIFICIAL INTELLIGENCE»,
      Lecture Notes in Computer ScienceTheory and Applications of Satisfiability Testing – SAT 2013,
      vol. 7962,
      2013
      , pp. 150-
      165
    101. Bozzano, Marco; Cimatti, Alessandro; Gario, Marco Elio Gustavo; Tonetta, Stefano,
      A Formal Framework for the Specification, Verification and Synthesis of Diagnosers,
      AAAI Workshops,
      2013
    102. 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
    103. Mover, Sergio; Cimatti, Alessandro; Tiwari, A.; Tonetta, Stefano,
      Time-aware Relational Abstractions for Hybrid Systems,
      Proceedings of the 13th International Conference on Embedded Software,
      2013
    104. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano,
      Parameter Synthesis with IC3,
      Formal Methods in Computer-Aided Design,
      2013
    105. Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian,
      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
    106. Cimatti, Alessandro; Dorigatti, Michele; Tonetta, Stefano,
      OCRA: A tool for checking the refinement of temporal contracts,
      in «AUTOMATED SOFTWARE ENGINEERING»,
      ASE 2013,
      2013
      , pp. 702-
      705
    107. Cimatti, Alessandro; Roveri, Marco; Susi, Angelo; Tonetta, Stefano,
      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
    108. Bittner, Benjamin; Bozzano, Marco; Cimatti, Alessandro; Xavier, Olive,
      Symbolic Synthesis of Observability Requirements for Diagnosability,
      Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence,
      AAAI Press,
      2012
    109. Cimatti, Alessandro; Griggio, Alberto,
      Software Model Checking via IC3,
      Proceedings of Computer Aided Verification - 24th International Conference, CAV 2012,
      Springer,
      vol. 7358,
      2012
    110. Cimatti, Alessandro; Raffaele, Corvino; Armando, Lazzaro; Narasamdya, Iman; Tiziana, Rizzo; Roveri, Marco; Angela, Sanseviero; Andrei, Tchaltsev,
      Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System,
      CAV,
      Springer,
      vol. 7358,
      2012
      , pp. 378-
      393
    111. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco,
      Verification of Parametric System Designs,
      2012
    112. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco,
      Software Model Checking with Explicit Scheduler and Symbolic Threads,
      in «LOGICAL METHODS IN COMPUTER SCIENCE»,
      vol. 8,
      2012
      , pp. 1-
      42
    113. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco,
      Solving Temporal Problems using SMT: Weak Controllability,
      Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence,
      AAAI Press,
      2012
    114. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco,
      Solving Temporal Problems using SMT: Strong Controllability,
      Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming,
      2012
    115. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano,
      SMT-Based Verification of Hybrid Systems,
      2012
    116. Cimatti, Alessandro; Tonetta, Stefano,
      A Property-Based Proof System for Contract-Based Design,
      2012
    117. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano,
      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
    118. Elena, Alaña; Héctor, Naranjo; Yuri, Yushtein; Bozzano, Marco; Cimatti, Alessandro; Gario, Marco Elio Gustavo; Régis de, Ferluc; Gérard, Garcia,
      Automated generation of FDIR for the compass integrated toolset (AUTOGEF),
      2012
    119. Cimatti, Alessandro; Sebastiani, Roberto,
      Theory and Applications of Satisfiability Testing – SAT 2012,
      in «LECTURE NOTES IN ARTIFICIAL INTELLIGENCE»,
      Springer,
      vol. 7317,
      2012
    120. Cimatti, Alessandro,
      Application of SMT solvers to hybrid system verification,
      Formal Methods in Computer-Aided Design, FMCAD 2012,
      IEEE,
      2012
      , pp. 4-
    121. 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
    122. Alessandro Cimatti; Angelo Susi; Stefano Tonetta; Marco Roveri,
      Formalizing requirements with object models and temporal constraints,
      in «SOFTWARE AND SYSTEMS MODELING»,
      Springer Berlin / Heidelberg,
      vol. 10,
      n. 2,
      2011
      , pp. 147-
      160
    123. Bozzano, Marco; Cimatti, Alessandro; Joost Pieter, Katoen; Viet Yen, Nguyen; Thomas, Noll; Roveri, Marco,
      Safety, Dependability and Performance Analysis of Extended AADL Models,
      in «COMPUTER JOURNAL»,
      vol. 54,
      n. 5,
      2011
      , pp. 754-
      775
    124. 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
    125. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto,
      Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories,
      in «THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH»,
      vol. 40,
      2011
      , pp. 701-
      728
    126. 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
    127. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano,
      Efficient Scenario VeriFIcation for Hybrid Automata,
      Efficient Scenario VeriFIcation for Hybrid Automata,
      2011
    128. Cimatti, Alessandro; Griggio, Alberto; Micheli, Andrea; Iman, Narasamdya; Roveri, Marco,
      Kratos - A Software Model Checker for SystemC,
      2011
    129. 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
    130. Daniele Campana; Alessandro Cimatti; Iman Narasamdya; Marco Roveri,
      An Analytic Evaluation of SystemC Encodings in Promela,
      2011
    131. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano,
      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
    132. Bozzano, Marco; Cimatti, Alessandro; O., Lisagor; Mattarei, Cristian; Mover, Sergio; Roveri, Marco; Tonetta, Stefano,
      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),
      EASST,
      vol. 46,
      2011
    133. Cavada, Roberto; Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco; Susi, Angelo; Tonetta, Stefano,
      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
    134. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano,
      HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction,
      2011
    135. Bittner, Benjamin; Bozzano, Marco; Cimatti, Alessandro; Xavier, Olive,
      Symbolic Synthesis of Observability Requirements for Diagnosability,
      Proceedings of 11th Symposium on Advanced Space Technologies in Robotics and Automation,
      2011
    136. 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
    137. Cimatti, Alessandro; Anders, Franzen; Griggio, Alberto; Kalyanasundaram, Krishnamani; Roveri, Marco,
      Tighter Integration of BDD and SMT for Predicate Abstraction,
      Proceedings of the Design, Automation & Test in Europe,
      2010
      , pp. 1707-
      1712
    138. Cimatti, Alessandro; Anders, Franzén; Griggio, Alberto; Sebastiani, Roberto; Cristian, Stenico,
      Satisfiability Modulo the Theory of Costs: Foundations and Applications,
      Proceedings of 16th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems,
      Springer,
      vol. 6015,
      2010
      , pp. 99-
      113
    139. 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
    140. 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
    141. 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
    142. Lei, Bu; Cimatti, Alessandro; Xuandong, Li; Mover, Sergio; Tonetta, Stefano,
      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
    143. Angelo, Chiappini; Cimatti, Alessandro; Macchi, Luca; Oscar, Rebollo; Roveri, Marco; Susi, Angelo; Tonetta, Stefano; Berardino, Vittorini,
      Formalization and validation of a subset of the European Train Control System,
      Proceedings of 32nd Int. Conference on Software Engineering,
      vol. 2,
      2010
      , pp. 109-
      118
    144. Cimatti, Alessandro; Micheli, Andrea; Narasamdya, Iman; Roveri, Marco,
      Verifying SystemC: a Software Model Checking Approach,
      Proceedings of the 10th Int. Conference on Formal Methods in Computer-Aided Design,
      2010
      , pp. 51-
      60
    145. Anders, Franzen; Cimatti, Alessandro; Alexander, Nadel; Sebastiani, Roberto; 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
    146. Bozzano, Marco; Cavada, Roberto; Cimatti, Alessandro; Joost Pieter, Katoen; Viet Yen, Nguyen; Thomas, Noll; Xavier, Olive,
      Formal Verification and Validation of AADL Model,
      2010
    147. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto,
      Efficient generation of craig interpolants in satisfiability modulo theories,
      in «ACM TRANSACTIONS ON COMPUTATIONAL LOGIC»,
      vol. 12,
      n. 1, article 7,
      2010
    148. Cimatti, Alessandro,
      SMT-Based Software Model Checking,
      SPIN,
      Springer-Verlag,
      vol. 6349,
      2010
      , pp. 1-
      3
    149. Roveri, Marco; Cimatti, Alessandro; Narasamdya, Iman; Micheli, Andrea; Daniele, Campana; Griggio, Alberto; Tchaltsev, Andrei,
      KRATOS,
      2010
    150. Bozzano, Marco; Cimatti, Alessandro; Joost Pieter, Katoen; Viet Yen, Nguyen; Thomas, Noll; Roveri, Marco; Ralf, Wimmer; Cavada, Roberto,
      COMPASS Tool,
      2010
    151. Thi Thieu Hoa, Le; Luigi, Palopoli; Roberto, Passerone; Ramadian, Yusi; Cimatti, Alessandro,
      Parametric Analysis of Distributed Firm Real-Time Systems: A Case Study,
      Proceedings of the 15th Int. Conference on Emerging Technologies and Factory Automation,
      2010
    152. 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
    153. Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano,
      Requirements Validation for Hybrid Systems,
      Proceedings 21st Int. Conference on Computer Aided Verification,
      Springer,
      vol. 5643,
      2009
      , pp. 188-
      203
    154. Bruttomesso, Roberto; Cimatti, Alessandro; Anders, Franzen; Griggio, Alberto; Sebastiani, Roberto,
      Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis. Extended version,
      in «ANNALS OF MATHEMATICS AND OF ARTIFICIAL INTELLIGENCE»,
      Springer,
      vol. 55,
      n. 1-2,
      2009
      , pp. 66-
      99
    155. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
      Codesign of Dependable Systems: A Component-Based Language,
      2009
    156. 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
    157. Cimatti, Alessandro; Jori Juhani, Dubrovin; Tommi Antero, Junttila; Roveri, Marco,
      Structure-Aware Computation of Predicate Abstraction,
      Proceedings of the Formal Methods in Computer Aided Design,
      2009
      , pp. 9-
      16
    158. 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
    159. Cavada, Roberto; Cimatti, Alessandro; Mariotti, Alessandro; Mattarei, Cristian; Micheli, Andrea; Mover, Sergio; Pensallorto, Marco; Roveri, Marco; Susi, Angelo; Tonetta, Stefano,
      Supporting Requirements Validation: The EuRailCheck Tool,
      Proceedings of 24th Int. Conference Automated Software Engineering,
      2009
      , pp. 665-
      667
    160. Bozzano, Marco; Cimatti, Alessandro; Roveri, Marco; Andrei, Tchaltsev,
      A Comprehensive Approach to On-Board Autonomy Verification and Validation,
      Workshop on Verification and Validation of Planning and Scheduling Systems,
      2009
      , pp. 1-
      10
    161. Bozzano, Marco; Cimatti, Alessandro; Joost Pieter, Katoen; Viet Yen, Nguyen; Thomas, Noll; Roveri, Marco,
      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
    162. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto,
      Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories,
      2009
    163. Dirk, Beyer; Cimatti, Alessandro; Griggio, Alberto; Erkan, Keremoglu; Sebastiani, Roberto,
      Software Model Checking via Large-Block Encoding,
      2009
    164. Bozzano, Marco; Cimatti, Alessandro; Roveri, Marco; 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,
      ACM,
      2009
      , pp. 285-
      286
    165. Bozzano, Marco; Cimatti, Alessandro; Joost Pieter, Katoen; Viet Yen, Nguyen; Thomas, Noll; Roveri, Marco,
      Model-Based Codesign of Critical Embedded Systems,
      Proceedings 2nd Int. Workshop on Model Based Architecting and Construction of Embedded Systems,
      CEUR-WS.org,
      vol. 507,
      2009
      , pp. 87-
      91
    166. 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,
      2009
      , pp. 121-
      130
    167. Roveri, Marco; Cimatti, Alessandro; Schuppan, Viktor; Tchaltsev, Andrei; Cavada, Roberto,
      NuGAT,
      2009
    168. Cimatti, Alessandro; Pistore, Marco; Traverso, Paolo,
      Automated Planning,
      Handbook of Knowledge Representation,
      Elsevier,
      2008
      , pp. 841-
      867
    169. Bruttomesso, Roberto; Cimatti, Alessandro; Anders, Franzen; Griggio, Alberto; Sebastiani, Roberto,
      The MathSAT 4SMT Solver,
      Proceedings of the 20th Int. Conference on Computer Aided Verification,
      Springer-Verlag,
      vol. 5123,
      2008
      , pp. 299-
      303
    170. 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
    171. 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
    172. Cimatti, Alessandro,
      Beyond Boolean SAT: Satisfiability Modulo Theories,
      Proceedings of the 9th Int. Workshop on Discrete Event Systems,
      IEEE Press,
      2008
      , pp. 68-
      73
    173. Cimatti, Alessandro; Luigi, Palopoli; Ramadian, Yusi,
      Symbolic Computation of Schedulability Regions using parametric timed automata,
      Proceeding of the 29th IEEE Real-Time Systems Symposium,
      IEEE Computer Society,
      2008
      , pp. 80-
      89
    174. Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano,
      Symbolic Compilation of PSL,
      in «IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS»,
      IEEE,
      vol. 27,
      n. 10,
      2008
      , pp. 1737-
      1750
    175. 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
    176. 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
    177. 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,
      2008
    178. Alessandro Cimatti; Andrea Guiotto; Marco Roveri,
      On Board Model Checking for Space Applications,
      Proceedings of ESA Workshop on Avionics Data, Control and Software Systems,
      2008
      , pp. 10-
      11
    179. Cimatti, Alessandro; Robert B., Jones,
      Formal Methods in Computer-Aided Design, Portland, Oregon, USA, 17-20 November 2008,
      IEEE,
      2008
    180. Cimatti, Alessandro; Bozzano, Marco; Adolfo, Villafiorita,
      FSAP,
      2008
    181. Bozzano, Marco; Cimatti, Alessandro; 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
    182. Zvonimir, Rakamaric; Bruttomesso, Roberto; Alan J., Hu; Cimatti, Alessandro,
      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
    183. 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
    184. Bruttomesso, Roberto; Cimatti, Alessandro; Anders, Franzen; Griggio, Alberto; Ziyad, Hanna; Alexander, Nadel; Amit, Palti; Sebastiani, Roberto,
      A Lazy and Layered SMT ({BV}) Solver for Hard Industrial Verification Problems,
      Proceedings of the 19th Int. Conference on Computer aided verification,
      Springer-Verlag,
      vol. 4590,
      2007
      , pp. 547-
      560
    185. 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,
      2007
      , pp. 69-
      76
    186. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto,
      A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories,
      Proceedings of the 10th Int. Conference on Theory and Applications of Satisfiability Testing,
      Springer,
      vol. 4501,
      2007
      , pp. 334-
      339
    187. 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
    188. Roderick, Bloem; Cimatti, Alessandro; Ingo, Pill; Roveri, Marco,
      Symbolic Implementation of Alternating Automata,
      in «INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE»,
      World Scientific Publishing,
      vol. 18,
      n. 4,
      2007
      , pp. 727-
      743
    189. Bertoli, Piergiorgio; Bozzano, Marco; Cimatti, Alessandro,
      A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis,
      Model Checking and Artificial Intelligence,
      Springer-Verlag,
      vol. 4428,
      2007
      , pp. 1-
      18
    190. Roberto, Bruttomesso; Cimatti, Alessandro; Roberto, Sebasatiani; Griggio, Alberto; Anders, Franzen,
      MathSAT,
      2007
    191. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Anders, Franzen; Ziyad, Hanna; Zurab, Khasidashvili; Amit, Palti; Sebastiani, Roberto,
      Encoding RTL Constructs for Mathsat: A preliminary report,
      Proceedings of 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning,
      vol. 144, issue 2,
      2006
      , pp. 3-
      14
    192. Bertoli, Piergiorgio; Cimatti, Alessandro; Roveri, Marco; Traverso, Paolo,
      Strong Planning under Partial Observability,
      in «ARTIFICIAL INTELLIGENCE»,
      Elsevier,
      vol. 170,
      n. 4-5,
      2006
      , pp. 337-
      384
    193. Marco, Bernardo; Cimatti, Alessandro,
      Formal Methods for Hardware Verification,
      Springer,
      vol. 3965,
      2006
    194. 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
    195. I. Pill; S. Semprini; R. Cavada; M. Roveri; R. Bloem; A. Cimatti,
      Formal analysis of hardware requirements,
      Proceedings of 43rd annual Design Automation Conference,
      2006
      , pp. 821-
      826
    196. Bertoli, Piergiorgio; Cimatti, Alessandro; Pistore, Marco,
      Strong Cyclic Planning Under Partial Observability,
      Proceedings of 17th European Conference on Artificial Intelligence,
      2006
      , pp. 580-
      584
    197. Armando, Alessandro; Cimatti, Alessandro,
      Post-workshop Proceedings of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning,
      in «ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE»,
      Electronic Notes in Theoretical Computer Science -- Elsevier,
      vol. 144,
      n. 2,
      2006
    198. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Tommi A., Junttila; Ranise, Silvio; Peter van, Rossum; Sebastiani, Roberto,
      Efficient theory combination via boolean search,
      in «INFORMATION AND COMPUTATION»,
      vol. 204,
      n. 10,
      2006
      , pp. 1493-
      1525
    199. 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
    200. 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
    201. Cimatti, Alessandro; Sebastiani, Roberto,
      Building Efficient Decision Procedures on top of SAT solvers,
      Formal Methods for Hardware Verification,
      Springer,
      vol. 3965,
      2006
      , pp. 144-
      175
    202. Armando, Alessandro; Cimatti, Alessandro,
      Preface. Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005),
      Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005),
      Elsevier B.V.,
      vol. Volume 144, Issue 2,
      2006
      , pp. 1-
      2
    203. 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
    204. Roberto, Bruttomesso; Cimatti, Alessandro; Anders, Franzen; Griggio, Alberto; Alessandro, Santuari; Sebastiani, Roberto,
      To Ackermann-ize or not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF U T),
      Proceedings of the 13th Int. Conference on 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning,
      2006
      , pp. 557-
      571
    205. Roberto, Bruttomesso; Cimatti, Alessandro; Anders, Franzen; Griggio, Alberto; Sebastiani, Roberto,
      Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis,
      Springer Verlag,
      vol. 4246,
      2006
      , pp. 527-
      541
    206. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; T. A., Junttila; Rossum Peter, Van; S. P., Schulz; Sebastiani, Roberto,
      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
    207. 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
    208. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; T., Antero Junttila; Ranise, Silvio; Rossum Peter, Van; Sebastiani, Roberto,
      Efficient Theory Combination via Boolean Search,
      2005
    209. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; T. A., Junttila; R., Peter van; S. P., Schulz; Sebastiani, Roberto,
      MathSAT: Thigt Integration of SAT and Mathematical Decision Procedures,
      2005
    210. Bozzano, Marco; R., Brutomesso; Cimatti, Alessandro; T. A., Junttila; Ranise, Silvio; Rossen Peter, Van; Sebastiani, Roberto,
      Efficient Satisfiability Modulo Theories via Delayed Theory Combination,
      2005
    211. Gilles, Audemard; Bozzano, Marco; Cimatti, Alessandro; Sebastiani, Roberto,
      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
    212. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Tommi, Junttila; Peter van, Rossum; Stephan, Schulz; Sebastiani, Roberto,
      Mathsat: Tight Integration of SAT and Mathematical Decision Procedures,
      in «JOURNAL OF AUTOMATED REASONING»,
      vol. 35,
      n. 1-3,
      2005
      , pp. 265-
      293
    213. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Tommi, Junttila; Ranise, Silvio; Peter van, Rossum; Sebastiani, Roberto,
      Efficient Satisfiability Modulo Theories via Delayed Theory Combination,
      Proceeding of 17th Int. Conference on Computer Aided Verification,
      Springer,
      vol. 3576,
      2005
      , pp. 335-
      349
    214. Marco Roveri; Alessandro Cimatti; Andrei Tchaltsev; Roberto Cavada; Simone Semprini; Roderick Bloem; Ingo Pill,
      RAT,
      2005
    215. Bertoli, Piergiorgio; Cimatti, Alessandro; Traverso, Paolo,
      Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains,
      Proceedings of 16th Eureopean Conference on Artificial Intelligence,
      2004
      , pp. 657-
      661
    216. Cimatti, Alessandro; Roveri, Marco; Bertoli, Piergiorgio,
      Conformant Planning via Symbolic Model Checking and Heuristic Search,
      in «ARTIFICIAL INTELLIGENCE»,
      vol. 159,
      n. 1-2,
      2004
      , pp. 127-
      206
    217. 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
    218. Bozzano, Marco; Cimatti, Alessandro; G., Colombini; V., Kirov; Sebastiani, Roberto,
      The MAthSAT Solver. A progress report,
      2004
    219. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Sebastiani, Roberto,
      The MathSAT Solver - a comparative evaluation,
      2004
    220. Roelofsen, Floris; Serafini, Luciano; Cimatti, Alessandro,
      Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems,
      Proceedings of 16th Eureopean Conference on Artificial Intelligence,
      2004
      , pp. 58-
      62
    221. Bozzano, Marco; Cimatti, Alessandro; Gabriele, Colombini; Veselin, Kirov; Sebastiani, Roberto,
      The MathSAT solver -- a progress report,
      Proceeding of 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning,
      2004
    222. Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso,
      Weak, Strong, and Strong Cyclic Planning via Symbolic Model Checking,
      in «ARTIFICIAL INTELLIGENCE»,
      Elsevier,
      vol. 147,
      n. 1-2,
      2003
    223. Bertoli, Piergiorgio; Cimatti, Alessandro; Pistore, Marco; Traverso, Paolo,
      A Framework for Planning with Extended Goals under Partial Observability,
      Proceedings of ICAPS`03 - 13th International Conference on Automated Planning and Scheduling,
      AAAI,
      2003
      , pp. 215-
      225
    224. Bertoli, Piergiorgio; Cimatti, Alessandro; Lago U., Dal; Pistore, Marco,
      Extending PDDL to mondeterminism, limited sensing and iterative conditional plans,
      2003
    225. Bozzano, Marco; Villafiorita Monteleone, Adolfo; O., Akerlund; P., Bieber; C., Bougnol; E., Boede; M., Bretschneider; A., Cavallo; C., Castel; M., Cifaldi; Cimatti, Alessandro; 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; Zacco, Gabriele,
      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
    226. Bertoli, Piergiorgio; Cimatti, Alessandro; Traverso, Paolo,
      Interleaving Execution and Planning via Symbolic Model Checking,
      ICAPS`03 Workshop on Planning under Uncertainty and Incomplete Information,
      AAAI,
      2003
      , pp. 1-
      7
    227. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso,
      MBP: A Model Based Planner,
      ICAPS`03: system demo session,
      2003
    228. Cimatti, Alessandro; C., Pecheur; Cavada, Roberto,
      Formal Verification of Diagnosability via Symbolic Model Checking,
      2003
    229. Bertoli, Piergiorgio; Cimatti, Alessandro; Lago U., Dal; Pistore, Marco,
      Extending PDDL to nondeterminism, limited sensing and iterative conditinal plans,
      ICAPS`03 Workshop on PDDL,
      2003
      , pp. 15-
      24
    230. Benedetti, Marco; Cimatti, Alessandro,
      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
    231. Cimatti, Alessandro; Charles, Pecheur; Cavada, Roberto,
      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
    232. Armin, Biere; Cimatti, Alessandro; E. M., Clarke; Ofer, Strichman; Yunshan, Zhu,
      Bounded Model Checking,
      in «ADVANCES IN COMPUTERS»,
      Academic Press,
      vol. 58,
      n. ISBN 0-12-012158-1,
      2003
      , pp. 118-
      149
    233. Audemard, Gilles; Bozzano, Marco; Cimatti, Alessandro; Sebastiani, Roberto,
      Verifying Industrial Hybrid Systems with MathSAT,
      CADE-19 Workshop: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR`03),
      2003
      , pp. 62-
      76
    234. 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
    235. Audemard, Gilles; Cimatti, Alessandro; Kornilowicz, Artur; Sebastiani, Roberto,
      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
    236. Cimatti, Alessandro; E., Giunchiglia; Roveri, Marco; Pistore, Marco; Sebastiani, Roberto; 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
    237. Bertoli, Piergiorgio; Cimatti, Alessandro; 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
    238. Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Kornilowicz, Artur; Sebastiani, Roberto,
      A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions,
      CADE-18 Conference on Automated Deduction,
      Springer,
      2002
      , pp. 195-
      210
    239. Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Kornilowicz, Artur; Sebastiani, Roberto,
      Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms and Requirements,
      CALCULEMUS-2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning,
      2002
      , pp. 157-
      192
    240. Cimatti, Alessandro; E. M., Clarke; Enrico, Giunchiglia; Fausto, Giunchiglia; Pistore, Marco; Roveri, Marco; 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
    241. Bertoli, Piergiorgio; Cimatti, Alessandro; Pistore, Marco; Traverso, Paolo,
      Plan Validation for Extended Goals under Partial Observability (preliminary report),
      Electronic Proceedings of AIPS`02 Workshop on Planning via Model Checking,
      2002
    242. Roveri, Marco; Cimatti, Alessandro; Cavada, Roberto; Tchaltsev, Andrei; Micheli, Andrea; Mariotti, Alessandro; Mover, Sergio; Marco, Pensallorto; Armando, Tacchella; Daniel, Sheridan; Gavin, Keighren; Tommi, Junttila; Timo, Latvala,
      NuSMV,
      2002
    243. 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
    244. Alessandro Cimatti,
      Industrial Applications of Model Checking,
      2001
    245. 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
    246. Cimatti, Alessandro; E., Giunchiglia; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; 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
    247. 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
    248. Massimo, Benerecetti; Cimatti, Alessandro,
      Symbolic model checking for multi-agent systems,
      Second Workshop on Computational Logic in Multi-Agent Systems (CLIMA`01),
      2001
    249. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso,
      MBP: a Model Based Planner,
      IJCAI-2001 Workshop on Planning under Uncertainty and Incomplete Information (PRO-2),
      2001
    250. Bertoli, Piergiorgio; Cimatti, Alessandro,
      Improving Heuristics for Planning and Search in Belief Space,
      2001
    251. Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri; Paolo Traverso,
      Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking,
      Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), Proceedings,
      Morgan Kaufmann,
      2001
      , pp. 473-
      478
    252. 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
    253. Alessandro Cimatti; Marco Roveri,
      Conformant Planning via Symbolic Model Checking,
      in «THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH»,
      AAAI Press,
      vol. 13,
      2000
      , pp. 305-
      338
    254. Alessandro Cimatti; Marco Roveri,
      Forward Conformant Planning via Symbolic Model Checking,
      AIPS 2000 Workshop on Model-Theoretic Approaches to Planning,
      2000
    255. Cimatti, Alessandro; Serafini, Luciano,
      A Context-Based Mechanization of Multi-Agent Reasoning,
      Formal Aspects of Context,
      Kluwer,
      vol. 20,
      2000
      , pp. 65-
      83
    256. V., Hartonas Garmhausen; E. M., Clarke; S., Campos; Cimatti, Alessandro; Giunchiglia, Fausto,
      Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints,
      in «SCIENCE OF COMPUTER PROGRAMMING»,
      Elsevier,
      vol. 36,
      2000
      , pp. 53-
      64
    257. Alessandro Cimatti; E.M. Clarke; Fausto Giunchiglia; Marco Roveri,
      NuSMV: a new symbolic model checker,
      in «INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER»,
      Springer,
      2000
      , pp. 410-
      425
    258. Alessandro Cimatti; Marco Roveri,
      Conformant Planning via Model Checking,
      Fifth European Conference on Planning [ECP`99],
      Springer,
      2000
      , pp. 21-
      34
    259. Cimatti, Alessandro; E. M., Clarke; Fausto, Giunchiglia; Roveri, Marco,
      NuSMV: a New Symbolic Model Verifier,
      11th International Conference on Computer Aided Verification (CAV`99), Proceedings,
      Springer,
      1999
    260. Cimatti, Alessandro; P. L., Pieraccini; Sebastiani, Roberto; Traverso, Paolo; Villafiorita Monteleone, Adolfo,
      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
    261. A., Chiappini; Cimatti, Alessandro; C., Porzia; G., Rotondo; Sebastiani, Roberto; Traverso, Paolo; Villafiorita Monteleone, Adolfo,
      Formal Specification and Development of a Safety-Critical Train Management,
      18th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1999),
      Springer,
      vol. 1698,
      1999
      , pp. 410-
      419
    262. Alessandro Cimatti; Marco Roveri,
      Conformant Planning via Model Checking,
      Fifth European Conference on Planning [ECP`99],
      Springer,
      1999
    263. Cimatti, Alessandro; Giunchiglia, Fausto; Traverso, Paolo; Villafiorita Monteleone, Adolfo,
      Run-Time Result Formal Verification of Safety Critical Software: an Industrial Case Study,
      FLoC`99 Workshop on Run-Time Result Verification,
      1999
    264. Cimatti, Alessandro; Giunchiglia, Fausto; R. W., Weyhrauch,
      A Many Sorted Natural Deduction,
      in «COMPUTATIONAL INTELLIGENCE»,
      Blackwell Publishing,
      vol. 1,
      n. 14,
      1998
      , pp. 135-
      150
    265. 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
    266. Alessandro Cimatti; Marco Roveri; Paolo Traverso,
      Strong Planning in Non-Deterministic Domains via Model Checking,
      Fourth International Conference on Artificial Intelligence Planning Systems [AIPS-98],
      1998
    267. 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
    268. Cimatti, Alessandro; Sebastiani, Roberto,
      Servizi forniti dagli strati Safety Layer e Connection Manager,
      1998
    269. Cimatti, Alessandro; Sebastiani, Roberto,
      Specifica formale dei protocolli Safety Layer e Connection Manager,
      1998
    270. Cimatti, Alessandro; Sebastiani, Roberto,
      Protocolli Safety Layer e Connection Manager: Descrizione del Codice SDL,
      1998
    271. Bertoli, Piergiorgio; Cimatti, Alessandro; Giunchiglia, Fausto; Traverso, Paolo,
      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
    272. Alessandro Cimatti; Fausto Giunchiglia; Marco Roveri,
      Abstraction in Planning via Model Checking,
      Symposium on Abstraction, Reformulation and Approximation (SARA 1998),
      1998
      , pp. 37-
      41
    273. Cimatti, Alessandro; Giunchiglia, Fausto; G., Mongardi; D., Romano; F., Torielli; Traverso, Paolo,
      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
    274. Cimatti, Alessandro; Giunchiglia, Fausto; G., Mongardi; D., Romano; F., Torielli; Traverso, Paolo,
      Formal Verification of a Railway Interlocking System Using Model Checking,
      in «FORMAL ASPECTS OF COMPUTING»,
      Springer,
      1998
      , pp. 361-
      380
    275. Alessandro Cimatti; Enrico Giunchiglia; Fausto Giunchiglia; Paolo Traverso,
      Planning via Model Checking: A Decision Procedure for AR,
      4th European Conference on Planning [ECP`97],
      Springer,
      vol. 1348,
      1997
      , pp. 130-
      142
    276. Cimatti, Alessandro; Giunchiglia, Fausto; G., Mongardi; B., Pietra; D., Romano; F., Torielli; Traverso, Paolo,
      Formal Validation of an Interlocking System for Large Railway Stations: A Case Study,
      1997
    277. Cimatti, Alessandro; Giunchiglia, Fausto; P., Pecchiari; B., Pietra; J., Profeta; D., Romano; Traverso, Paolo; 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
    278. Cimatti, Alessandro; Enrico, Giunchiglia; Giunchiglia, Fausto; Traverso, Paolo,
      A Model Based Decision Procedure for Common Sense Temporal Reasoning,
      1997
    279. Cimatti, Alessandro; Giunchiglia, Fausto; G., Mongardi; D., Romano; F., Torielli; Traverso, Paolo,
      Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System,
      Third International SPIN Workshop [SPIN97],
      1997
    280. Cimatti, Alessandro; Giunchiglia, Fausto; G., Mongardi; B., Pietra; D., Romano; F., Torielli; Traverso, Paolo,
      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
    281. Bertoli, Piergiorgio; Cimatti, Alessandro; Giunchiglia, Fausto; Traverso, Paolo,
      Certification of Translators via Off-line and On-line Proof Logging and Checking,
      1997
    282. Cimatti, Alessandro; Traverso, Paolo,
      Computational Reflection via Mechanized Logical Deduction,
      in «INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS»,
      Wiley,
      vol. 11,
      n. 5,
      1996
      , pp. 279-
      293
    283. Enrico, Giunchiglia; Armando, Alessandro; Traverso, Paolo; Cimatti, Alessandro,
      Visual Representation of Natural Language Scene Descriptions,
      in «IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS»,
      IEEE,
      vol. 26,
      n. 8,
      1996
      , pp. 279-
      293
    284. Bouquet, Paolo; Cimatti, Alessandro,
      Mechanizing Local Reasoning with Contexts,
      Working notes of the IJCAI-95 Workshop on ``Modelling Context in Knowledge Representation and Reasoning``,
      1996
      , pp. 13-
      23
    285. Cimatti, Alessandro; Serafini, Luciano,
      Mechanizing Multi-Agent Reasoning with Belief Contexts,
      Practical Reasoning, International Conference on Formal and Applied Practical Reasoning [FAPR`96],
      Springer,
      1996
      , pp. 694-
      696
    286. Massimo, Benerecetti; Cimatti, Alessandro; Enrico, Giunchiglia; Giunchiglia, Fausto; Serafini, Luciano,
      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
    287. Armando, Alessandro; Cimatti, Alessandro; E., Giunchiglia; P., Pecchiari; L., Spalazzi; Traverso, Paolo,
      Flexible Planning by Integrating Multilevel Reasoning,
      in «ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE»,
      Elsevier,
      vol. 4,
      1995
      , pp. 401-
      412
    288. Giuliano, Antoniol; Caprile, Bruno Giovanni; Cimatti, Alessandro; 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
    289. Cimatti, Alessandro; Serafini, Luciano,
      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
    290. Cimatti, Alessandro; Serafini, Luciano,
      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
    291. Cimatti, Alessandro; Serafini, Luciano,
      Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance,
      First International Conference on Multiagent Systems,
      MIT Press,
      1995
      , pp. 57-
      64
    292. Traverso, Paolo; Cimatti, Alessandro; Luca, Spalazzi; Enrico, Giunchiglia; Armando, Alessandro,
      MRG: Building planners for real world complex applications,
      in «APPLIED ARTIFICIAL INTELLIGENCE»,
      Taylor and Francis,
      1994
      , pp. 333-
      357
    293. Giunchiglia, Fausto; Armando, Alessandro; Cimatti, Alessandro; Traverso, Paolo,
      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
    294. Cimatti, Alessandro; Giunchiglia, Fausto; G., Mongardi; D., Romano; F., Torielli; Traverso, Paolo,
      Valutazione del CBR-tool orientato all`help desk `Case Advisor`,
      1993
    295. Giunchiglia, Fausto; Traverso, Paolo; Cimatti, Alessandro; Luca, Spalazzi; Sandro, Dalbosco; Serafini, Luciano; Enrico, Giunchiglia; Alessandro, Armando; Paolo, Pecchiari,
      MRG: sistema di ragionamento,
      in «AUTOMAZIONE E STRUMENTAZIONE»,
      VNU Business Publications,
      vol. 9,
      1993
      , pp. 97-
      103
    296. Giunchiglia, Fausto; Traverso, Paolo; Cimatti, Alessandro; Luca, Spalazzi; Sandro, Dalbosco; Serafini, Luciano; Enrico, Giunchiglia; Armando, Alessandro; Paolo, Pecchiari,
      MRG: un nucleo di ragionamento per un sistema integrato multifunzionale,
      in «SISTEMI INTELLIGENTI»,
      il Mulino,
      vol. 3,
      1993
      , pp. 435-
      460
    297. Traverso, Paolo; Luca, Spalazzi; Cimatti, Alessandro,
      A planning language and a semantics for real world autonomous agents,
      1993 Italian Planning Workshop,
      1993
    298. Traverso, Paolo; Cimatti, Alessandro; Luca, Spalazzi,
      Beyond the single planning paradigm: introspective planning,
      10th European Conference on Artificial Intelligence (ECAI 1992),
      Wiley,
      1992
      , pp. 643-
      647
    299. Luca, Spalazzi; Cimatti, Alessandro; Traverso, Paolo,
      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
    300. Traverso, Paolo; Cimatti, Alessandro; 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
    301. Cimatti, Alessandro; Traverso, Paolo; Luca, Spalazzi,
      Programming Planners with Flexible Architectures,
      AI and Cognitive Science `92,
      Springer Verlag,
      1992
      , pp. 311-
      314
    302. Cimatti, Alessandro; Traverso, Paolo; Sandro, Dalbosco; Armando, Alessandro,
      Navigation by Combining Reactivity and Planning,
      Intelligent Vechicles `92 Symposium,
      IEEE Industrial Electronics,
      1992
      , pp. 265-
      270
    303. Giunchiglia, Fausto; Traverso, Paolo; Cimatti, Alessandro; Paolo, Pecchiari,
      A System for Multi-Level Reasoning,
      IMSA `92, International Workshop on New Models for Software Architecture,
      1992
      , pp. 190-
      195
    304. Giunchiglia, Fausto; Traverso, Paolo; Cimatti, Alessandro; Luca, Spalazzi,
      Tactics: extending the notion of plan,
      ECAI-92 Workshop `Beyond Sequential Planning`,
      1992
    305. Giunchiglia, Fausto; Traverso, Paolo; Cimatti, Alessandro; Luca, Spalazzi; Sandro, Dalbosco; Serafini, Luciano; Enrico, Giunchiglia; Armando, Alessandro; 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
    306. Giunchiglia, Fausto; Cimatti, Alessandro; Sandro, Dalbosco; Traverso, Paolo; 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