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
    higher-order)).
  • 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".
  • 2022-2025: EUR EIPHI project TACTICQ (Techniques Avancées de Calcul pour la Théorie de l'Information et du Contrôle Quantiques) supported by the French program "Investissements d’Avenir".
  • 2022-2027: PEPR project EPiQ (Étude de la Pile Quantique : algorithmes, modèles de calcul et simulation pour l'informatique quantique), part of the French Plan Quantique 2030.

Teaching

  • Logics and Deduction, 52 hours, license in computer science, until August 2020
  • Formal Methods, 69 hours, license in computer science, e-learning
  • Specification and Verification of Programs (with Why3), 27 hours, license in computer science, e-learning
  • Specification and Verification of Programs (with KeY prover), 58 hours, master in computer science
  • Initiation to research in computer science, 18 hours, option of the master in computer science
  • Specification and Automated Verification of Models (LTL, model-checking), 13 hours, master in computer science, until August 2020
  • Specify and Verify (reactive systems and imperative programs, with Cubicle and Why3), 27 hours, master in computer science, e-learning. Presented at FMTea 2023, workshop affiliated with FM 2023. Some course materials are shared in this archive: svfmtea2023presentedcoursematerial.zip.

Software

Click on items in the right menu for more informations.