3 postdoctorial position in quantum programming / program analysis / formal methods, Paris (France)

The CEA LIST, Software Security Lab (LSL) at the Université Paris-Saclay, has several open 3 years postdoc positions in the area of Formal verification for quantum programming, to begin as soon as possible at Paris-Saclay, France. It is articulated around the Qbricks tool, which aims at providing an automated solution for quantum programming formal verification. 

The positions are expected to start in October 2024.

In these positions, we are interested in verification mechanisms aiming at ensuring that a quantum program implementation indeed satisfies its intended behaviour. Possibilities include, among others:
- high-level automatic verification of quantum programs for implicit program properties,
- design of verification oriented hybrid quantum programming languages
- high-level functional reasoning for quantum programs,
- circuit-level automatic verification of quantum programs,
- verification of circuit transformation and compilation.