En poursuivant votre navigation sur ce site, vous acceptez le dépôt de cookies dans votre navigateur. (En savoir plus)
Portail > Offres > Offre UMR9021-MARGRA-003 - Post-doctorat (H/F) : Analyse et vérification des systèmes d'addition de vecteurs d'entiers et de leurs extensions.

Post-doctorate (M / F): Analysis and verification of integer vector addition systems and their extensions

This offer is available in the following languages:
Français - Anglais

Date Limite Candidature : mardi 27 décembre 2022

Assurez-vous que votre profil candidat soit correctement renseigné avant de postuler. Les informations de votre profil complètent celles associées à chaque candidature. Afin d’augmenter votre visibilité sur notre Portail Emploi et ainsi permettre aux recruteurs de consulter votre profil candidat, vous avez la possibilité de déposer votre CV dans notre CVThèque en un clic !

General information

Reference : UMR9021-MARGRA-003
Workplace : GIF SUR YVETTE
Date of publication : Tuesday, November 15, 2022
Type of Contract : FTC Scientist
Contract Period : 5 months
Expected date of employment : 1 February 2023
Proportion of work : Full time
Remuneration : between € 2,500 gross monthly and € 3,500 gross monthly depending on experience
Desired level of education : PhD
Experience required : 1 to 4 years


As part of the ANR BRAVAS project, we are interested in the analysis and verification of addition systems of integer vectors and their extensions.


- Analysis and verification of vector addition systems.
- Analysis and verification of counting machines and their extensions.
- Algorithmic of accessibility properties.


The recruited person must have skills in:
- Logic, automata and formal verification
- Algorithmic verification
- Competing models

Work Context

The post-doctoral fellow will work in the LMF laboratory. The Formal Methods Laboratory (LMF) is a computer science laboratory specialized in the development of formal methods. It has three main supervisors (CNRS, Université Paris-Saclay, ENS Paris-Saclay) and two partners (Inria, CentraleSupélec). Its ambition is to shed light on the "digital world" through mathematical logic by using formal methods as a tool for analysis, modeling and reasoning for computer programs, security protocols, etc. It relies on computational paradigms ranging from the most classical to the most innovative such as quantum computing. The LMF is structured in poles: its core business includes two, "Proofs and languages" and "Models"; the third, "Interactions", is an opening to other fields such as artificial intelligence or biology. It is one of the world's leading laboratories in its field.

The LMF is located on the Moulon plateau (91), in the premises of the ENS Paris-Saclay and in the 650 building of the University of Paris-Saclay.
The laboratory is composed of about one hundred members, including fifty researchers (CNRS, Inria) or teacher-researchers (Université Paris-Saclay, ENS Paris-Saclay, CentraleSupélec).
The recruited post-doctoral fellow will work in the Model checking team, whose objective is the development of models, logic, algorithms and verification tools.

Constraints and risks

screen work

We talk about it on Twitter!