I am a researcher in the Embedded Systems Unit of FBK.

Contact information

Embedded Systems Unit
Fondazione Bruno Kessler
Via Sommarive 18
38123 Povo (TN) -- Italy
Tel. (+39) 0461 314359


  • Model checking of temporal logics
  • Satisfiability of temporal logics
  • Formal methods for requirements validation
  • Contract-based design
  • SMT-based hybrid systems verification
  • SMT-based verification of symbolic transition systems
  • Safety and security

The DBLP list of my publications is available here

Recent Publications

  • Contracts-refinement proof system for component-based embedded systems: A. Cimatti, S. Tonetta. Sci. Comput. Program. (2015). In press.
  • M. Bozzano, A. Cimatti, O. Lisagor, C. Mattarei, S. Mover, M. Roveri, S. Tonetta: Safety assessment of AltaRica models via symbolic model checking. Sci. Comput. Program. 98: 464-483 (2015)
  • A. Cimatti, S. Mover, S. Tonetta: Quantifier-free encoding of invariants for hybrid systems. Formal Methods in System Design 45(2): 165-188 (2014)
  • Formal Safety Assessment via Contract-Based Design: M. Bozzano, A. Cimatti, C. Mattarei, S. Tonetta. ATVA 2014.
  • Making Implicit Safety Requirements Explicit. An AUTOSAR Safety Case: T. Arts, M. Dorigatti, S. Tonetta SAFECOMP 2014.
  • The nuXmv Symbolic Model Checker: R. Cavada,A. Cimatti,M. Dorigatti,A. Griggio,A. Mariotti,A. Micheli,S. Mover,M. Roveri, S. Tonetta. CAV 2014.
  • Verifying LTL Properties of Hybrid Systems with K-Liveness: A. Cimatti,A. Griggio,S. Mover,S. Tonetta. CAV 2014.
  • IC3 Modulo Theories via Implicit Predicate Abstraction: A. Cimatti,A. Griggio,S. Mover,S. Tonetta. TACAS 2014.
  • Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic: M. Bozzano, A. Cimatti, M. Gario, S. Tonetta. TACAS 2014





Co-recipient of the following awards:

  • 2012 FMCAD Best Paper Award
  • 2010 FBK Stringa Award
  • 2010 Microsoft Research SEIF Award