Applications are invited for PhD student or postdoc positions at Ecole Polytechnique in Paris, France. The successful candidates will work under the supervision of Sylvie Putot (http://www.lix.polytechnique.fr/Labo/Sylvie.Putot/index.html) and Eric Goubault (http://www.lix.polytechnique.fr/Labo/Eric.Goubault/) on formal verification and analysis techniques of neural networks (used for classification or as part of a larger cyber-physical system). The students will interact also with the project members of the SAIF project https://project.inria.fr/saif/project-members/ through regular project meetings. The particular research topic will be determined based on the common interests of the candidate and the supervisors, and can be either theoretical or practical. Possible themes in the area of formal methods for robustness and explainability of AI include the analysis of ReLU activated neural networks (possibly using tropical methods), generalized reachability problems and hyperproperties, probabilistic properties and imprecise probabilities etc. Candidates should have a strong background in computer science with an interest in formal methods, abstract interpretation/set-based methods, artificial intelligence, cyber-physical systems... Interested candidates should send their application (CV, references, motivation letter) via e-mail at {sylvie.putot,eric.goubault}@polytechnique.edu