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

  • INRIA CASSIS
  • Project INTERREG OSCAR (Optimization, Simulation, Control and Applications of AFM arrays) on modeling of arrays of atomic force microscopes (AFM).
  • ANR GECCOO
  • PSIRob 2006 smart surface project: Generic modeling of interactions between an object and a micro-conveying surface consisting of an array of MEMS.
  • ARC CeProMi (Certification of Programs manipulating Memory (modularity, Invariants, refinement, Effects and
    Higher-Order)).

Teaching

  • 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

Software

Click on items in the right menu for more informations.