PhD Position F/M Campagne Doctorant: verification of Linux kernel source code

Contract type : Fixed-term contract

Level of qualifications required : Graduate degree or equivalent

Fonction : PhD Position

Assignment

Understand the opportunities and challenges that arise in verifying the source code of an existing OS.

Design and implement tools to facilitate such verification.

Consider how a verification effort can scale, across time and to larger code fragments.

Main activities

Study of Linux kernel source code.

Design and implementation of program analyses.

Construction and validation of specifications for Linux kernel source code.

Skills

Familiarity with programming in C and OCaml.

Familiarity with program verification tools such as Frama-C.

Familiarity with operating systems concepts and the Linux kernel code base.

Strong research skills, in terms of reading research papers, writing research papers, and making presentations.

Benefits package

  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
  • Possibility of teleworking
  • Flexible organization of working hours 12after 6 months of employment) 
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage

Remuneration

According to civil service salary scales