Main page

Welcome in the personal webpages of Alain Giorgetti

Research interests

  • Deductive verification of safety properties.
  • Translation of temporal properties into JML annotations.
  • More generally, formal methods for program verification and theorem proving.

Project participations

  • 2002-2015: Team-project INRIA CASSIS (Combinaisons d'Approches pour la Sécurité des Systèmes InfiniS).
  • 2004-2008: ANR GECCOO (Génération de code certifié pour des applications orientées objet).
  • 2007-2009: ARC CeProMi (Certification of Programs manipulating Memory (modularity, Invariants, refinement, effects and
  • 2007-2010: PSIRob 2006 smart surface project, generic modeling of interactions between an object and a micro-conveying surface consisting of an array of MEMS.
  • 2010-2012: Project INTERREG OSCAR (Optimization, Simulation, Control and Applications of AFM arrays) on modeling of arrays of atomic force microscopes (AFM).
  • 2017-2020:  ISITE-UBFC project I-QUINS (Integrated QUantum Information at the NanoScale) supported by the French program "Investissements d’Avenir".


  • Program Proofs, 58 hours, master in computer science
  • Decision Procedures, 13 hours, master in computer science
  • Logics and Deduction, 52 hours, license in computer science
  • Formal Methods, 81 hours, license in computer science, e-learning


Click on items in the right menu for more informations.