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
- AutoCheck, random and enumerative testing tool for OCaml and WhyML properties.
- Project page on github: https://github.com/alaingiorgetti/autocheck
- Project page on github: https://github.com/alaingiorgetti/autocheck
- cut: A library for Coq unit testing
- enum: A library of verified sequential generation C programs.
- Project page on github, for releases > 1.0: https://github.com/alaingiorgetti/enum
- Former releases: enum.0.1.tar.gz, enum.0.2.tar.gz, enum.0.3.tar.gz, enum-1.0.tar.gz.
Click on items in the right menu for more informations.