[TYPES/announce] Two positions (one PhD and one Postdoc) in quantum formal verification @ Université Paris-Saclay, CEA List, France

[BARDIN Sébastien]

The emerging quantum software group @ CEA List, Université Paris-Saclay, offers 2 fully-funded  positions at the crossroad of quantum programming, program analysis and formal methods.


=== OUR GROUP

We are an emerging group in formal verification and static analysis of quantum programs, integrated in the Software Safety Laboratory of CEA List, Université Paris-Saclay. Our long term goal is to design and develop formal techniques and tools enabling productive and certified quantum programming. Especially, we develop Qbricks [1], a proof of concept environment for formally verified quantum programming language.

See our website at https://qbricks.github.io/ for additional information.


=== Position#1 (3 years PhD) Probing quantum verification in the NISQ era

The goal of this doctoral position is to probe formal verification against first generation of quantum application (NISQ era). Possibilities include, among other: extending Qbricks semantic and proof model to the hybrid paradigm, develop and implement a specification and proof system for error propagation and correction in quantum computing, develop  certified ready-to-use NISQ applications.

Keywords: quantum programming,  formal verification, NISQ, quantum error correction


=== Position#2 (2 years PostDoc)

The goal of this post-doctoral position is to extend  formal verification practice to quantum compilation.  Possibilities include, among others, error correction mechanisms in certified quantum code, together with specifications and reasoning technique for certifying its reliability, automatized certified optimizer for quantum circuits, hardware agnostic assembly language together with its compiler,

Keywords: quantum programming, compilation, optimization, formal verification


=== HOW TO APPLY

Applications should be sent to sebastien.bardin at cea.fr as soon as possible (first come, first served) and by early July 2021 at the latest. Candidates should send a CV, a cover letter, a transcript of all their university results, as well as contact information of two references. Each  position is expected to start in October 2021.

Advisors: Sébastien Bardin (CEA), Christophe Chareton (CEA)
Contact: sebastien.bardin at cea.fr


[1] C. Chareton, S. Bardin, F. Bobot, V. Perrelle, and B. Valiron. An Automated Deductive Verification Framework for Circuit-building Quantum Programs. ESOP 2021.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210530/78b152d5/attachment.htm>