Jobs – LMV Team

Open positions

Maître de conférences

Concours 2025 : poste de Maître de conférences susceptible d’être ouvert au concours dans l’équipe LMV

PhD Funding / Financement de thèses

PhD (RA positions) opportunities in the LMV team:
– in collaboration with CEA (job location: CEA List, Saclay) Runtime Verification of Multistate Properties, supervisors: Julien Signoles, Jan Rochel, Frédéric Loulergue
– in collaboration with Thales (job location: Thales Research & Technology, Saclay), Vérification de modules critiques d’hyperviseur avec la prise en compte des propriétés matérielles, supervisors: Nikolai Kosmatov, Frédéric Loulergue
– in collaboration with ONERA, Vérification formelle d’une librairie distribuée de manipulation de maillage, supervisors : Michael Lienhardt (Onera) et Frédéric Loulergue (Université d’Orléans and not J. Signoles CEA as mentioned in the proposal)

Other

Postdoctoral and engineer positions will open in the context of the ForCoaLa project from Spring 2025.

Past offers

March 2025
Ingénieur de recherche CDD 12 mois, LIFO, Orléans: Vérification Dynamique de propriétés de Sécurité

Le projet VéDySec

Le poste est ouvert dans le cadre du projet collaboratif ASTRID Maturation VéDySec (https://anr.fr/Projet-ANR-24-ASM2-0001) réunissant le LIFO, Université d’Orléans (https://www.univ-orleans.fr/lifo), le CEA List (https://list.cea.fr/en/) et Thales (https://www.thalesgroup.com/en).

Les menaces de sécurité sont devenues une préoccupation majeure dans les dernières années. Une faille de sécurité peut être exploitée par des attaquants et leur permettre de récupérer des
données confidentielles (données personnelles, médicales ou bancaires ; secrets industriels ou défense ; clefs de chiffrement, etc.), d’avoir accès aux services sans y être autorisés, ou de
modifier ou corrompre des données sensibles dans un objectif malveillant (usurpation d’identité, espionnage, contournement des contrôles d’accès, volonté de nuisance, guerres hybrides, attentats, etc.).

Les techniques de vérification statique formelle, notamment par interprétation abstraite ou par vérification déductive, peuvent permettre de démontrer l’absence de vulnérabilités dans un logiciel. Cependant, ces techniques restent complexes à appliquer sur des logiciels industriels. En effet, leurs applications nécessitent une expertise très pointue et demande beaucoup de temps, ce qui engendre un coût très élevé. Dans ce contexte, développer des techniques de vérification dynamique de propriétés de sécurité — plus facile et plus rapide à utiliser que la vérification statique — est nécessaire pour pouvoir appliquer ces techniques à un plus large spectre de projets. La maturation de ces techniques permettra de sécuriser un plus grand nombre de produits, de réduire le nombre de failles de sécurité et par conséquent de diminuer les risques d’attaques sur les logiciels concernés.

Le principal objectif du projet VéDySec est la maturation de l’outillage et la consolidation des méthodologies d’application pour la spécification et la vérification dynamique de propriétés de sécurité afin d’amener cette technologie au TRL 6.

Diplômes et compétences requis

Master ou doctorat (soutenu ou à soutenir prochainement) en informatique
Compétences en vérification déductive, de préférence de programmes C
Compétences en vérification dynamique, de préférence de programmes C
Compétences en programmation fonctionnelle, de préférence en OCaml
Capacité de communication et de travail en équipe
Anglais professionnel (oral et écrit)

Le poste est disponible immédiatement, les candidatures seront examinées jusqu’à ce qu’un recrutement soit réalisé.

Toute question et les candidatures (CV académique et les coordonnées de deux personnes pouvant fournir une recommandation) sont à envoyer à Frederic Loulergue (Frederic.Loulergue@univ-orleans.fr).

June 2024

L’université d’Orléans propose actuellement un poste d’enseignant-chercheur contractuel en informatique, avec prise de poste au 01/10/2024.

Le service d’enseignement s’effectuera en priorité au département d’informatique de l’UFR Sciences et Techniques.
L’intégration en recherche s’effectuera dans l’une des équipes du laboratoire LIFO (https://www.univ-orleans.fr/lifo/) dans l’une de ces équipes : CA : Contraintes et Apprentissage (IA); GAMoC : Graphes, Algorithmes, et Modèles de Calcul; LMV : Langages, Modélisation et Vérification; Pamda : Parallélisme et gestion de données (Big Data).

Ce poste offre une opportunité à un docteur d’enrichir son expérience de recherche et d’enseignement. Nous cherchons des candidats pouvant s’intégrer à l’une de nos équipes de recherche, en participants aux projets mentionnés dans la fiche de poste. L’objectif est de permettre à la personne recrutée de s’investir en recherche et d’augmenter sa production scientifique en collaboration avec l’une de nos équipes.
La fiche de poste et les modalités de candidature sont disponibles ici : http://www.univ-orleans.fr/upload/public/2024-05/2024_UFR_ST_LIFO_INFORMATIQUE.pdf

Il est recommandé de prendre contact avec l’équipe d’accueil, ainsi qu’avec la direction du département d’informatique (voir fiche de poste pour les contacts).

Le candidat doit être titulaire du doctorat. Le poste est pour 11 mois, renouvelable deux fois un an. La rémunération est proche de la grille des maître de conférences, avec une éventuelle prise en compte de l’expérience après la thèse. Le service d’enseignement sur une année pleine est de 192h équivalent TD (max. 50h complémentaires). Des charges administratives peuvent éventuellement être confiées à la personne recrutée (ouvrant à des éventuelles primes).

January 2024

Two postdoctoral researcher positions are available at the University of Orléans, France.

The successful candidates will be members of the LMV team https://www.univ-orleans.fr/lifo/equipes/lmv/ of the Computer Science Laboratory of Orléans (LIFO https://www.univ-orleans.fr/lifo/?lang=en), Orléans site. The city is in the heart of the Loire Valley https://www.tourisme-orleansmetropole.com/en/visit-orleans-get-inspired/loire-valley/orleans-in-the-heart-of-the-loire-valley, an outstanding cultural landscape classified as a UNESCO World Heritage Site in 2000.

CoMeMoV Project

A Post-Doctoral position is available as part of the CoMeMoV https://comemov.github.io project between LIFO https://www.univ-orleans.fr/lifo/?lang=en (University of Orleans, France), CEA List https://list.cea.fr/en and Thales Research and Technology https://www.thalesgroup.com/en/global/innovation/research-and-technology.

Frama-C https://www.frama-c.com/ is an extensible and collaborative open-source platform dedicated to source-code analysis of C software. If offers a specification language and various analyzers in the form of separate plugins. The WP plugin of Frama-C can be used to prove that a given C program respects its specification. WP provides a combination of different memory models that collaborate together thanks to a smart but simple partitioning of the memory. On moderately complex, industrial-strength programs, this combination already makes WP mature enough to be deployed for proving critical industrial embedded software. However, several theoretical and practical issues still persist.

The goal of CoMeMoV is to tackle these issues to allow deductive verification with WP to better scale on complex industrial programs. The work of the successful candidate will mainly focus on the formalization and proof of correctness of the proposed collaborative memory models for deductive verification (WP3).

Application requirements:

PhD (obtained or to be obtained soon) in Computer Science

Technical background in formal methods, in particular, in interactive theorem proving

Technical background in programming in C
Communication skills and teamwork capabilities
English language fluency in both speaking and writing

The position is available immediately. This is a research-only position, for 21 months. Please send the application materials (CV and cover letter) or any questions to Frederic Loulerge .

The deadline for application is December 23, 2023.

AcceptAlgo Project

A Post-Doctoral position is available as part of the AcceptAlgo, a two-year project funded by Région Centre Val de Loire. The partners are two institutes of the University of Orleans: the Orleans Economics Laboratory (LEO https://www.leo-univ-orleans.fr/en/) and the Computer Science Laboratory of Orleans (LIFO https://www.univ-orleans.fr/lifo/?lang=en).

Individuals have seen their exposure to algorithms increase considerably over the past decade. This exposure is exercised mainly in direct interaction with computers, telephones or other connected objects, during many moments of the social and economic life of individuals, but also in administrative or technical procedures of professionals. Individuals interact with algorithms when searching for information on the internet, when using connected medical devices, when delegating the management of their savings and retirement or when making online purchases. This research project aims to study how individuals evaluate and accept algorithms presented in mathematical form and in simple language form i.e. with words intelligible by individuals. It consists in measuring the acceptability for individuals of the algorithms presented through these simplified explanations.

The role of the postdoctoral researcher in this project is to improve and extend SyDPaCC https://sydpacc.github.io, a framework for the Coq proof assistant to develop correct functional scalable parallel programs from sequential specifications.