Welcome in the personal webpages of Alain Giorgetti
- Deductive verification of safety properties.
- Translation of temporal properties into JML annotations.
- More generally, formal methods for program verification and theorem proving.
- 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
- 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
- enum: A library of verified sequential generation C programs. With Richard Genestier.
- cut: A library for Coq unit testing
Click on items in the right menu for more informations.