More precisely, its works will focus on formal verification of deterministic and probabilistic properties of AltaRica 3.0 models, with an extension on stochastic simulation. Benjamin will be supervised by Antoine RAUZY (chaire Blériot-Fabre – Ecole Centrale-Supelec), Jean-Marc ROUSSEL (LURPA – ENS Cachan) and Michel BATTEUX (Projet OpenAltaRica – IRT SystemX).