Dear list,

The Software Security and Reliability Lab (LSL) at CEA Paris Saclay has several open positions (to start as soon  as possible) to work in the Frama-C team!

Frama-C (https://www.frama-c.com/) is an open-source sound static and dynamic analysis platform targeting C/C++ source code. It relies on advanced techniques such as abstract interpretation and theorem proving. The platform has been used in academia and the industry for safety and
security purposes, to prevent various vulnerabilities, and to prove functional properties on small and large codebases.

Open positions:

• 3-year engineer position: Apply Frama-C on case studies for cybersecurity purposes, extend Frama-C for cybersecurity purposes
  https://www.frama-c.com/jobs/2023-02-28-fixed-term-use-case.html
  (OCaml, C, formal methods, cybersecurity)
• 3-year engineer position: Improve the new Frama-C GUI, port existing Frama-C plug-ins to the GUI and create new ways of browsing analysis results
  https://www.frama-c.com/jobs/2023-02-28-fixed-term-ivette.html
  (TypeScript, Electron, ReactJS, OCaml)
• 3-year computer scientist position: Develop and extend the formal analysis capabilities of Frama-C, in particular the WP and Eva plug-ins
  https://www.frama-c.com/jobs/2023-02-28-fixed-term-analysis.html
  (OCaml, Formal Methods, Deductive Verification, Abstract Interpretation)
• 3-year computer scientist position: Improve the kernel of Frama-C, in particular in order to improve its ability to deal with large and complex code bases.
  https://www.frama-c.com/jobs/2023-02-28-fixed-term-kernel.html
  (OCaml, Formal Methods, Language Semantics)

Feel free to contact me for additional details.

Best,
Allan, for the Frama-C team