<div dir="ltr">The emerging quantum software group @ CEA List, Université Paris-Saclay, offers <br>a two years fully-funded postdoctoral position at the crossroad of quantum <br>programming, program analysis and formal methods.<br><br><br>=== OUR GROUP<br><br>We are an emerging group in formal verification and static analysis of quantum <br>programs, integrated in the Software Safety Laboratory of CEA List, Université <br>Paris-Saclay. Our long term goal is to design and develop formal techniques and <br>tools enabling productive and certified quantum programming. Especially, we <br>develop Qbricks [1], a proof of concept environment for formally verified <br>quantum programming language.<br><br>See our website at <a href="https://urldefense.com/v3/__https://qbricks.github.io/__;!!IBzWLUs!DTmRMuyfh6ehH9DSFJaqLMIs4YlesQRyI8Q8dkpjvQlB5Tx-NTs4Fg265PDuyMEj-jAvzHF-RqvC7g$">https://qbricks.github.io/</a> for additional information.<br><br>=== ABOUT THE POSTDOC POSITION<br><br>Adapting the best practice for classical computing formal verification -- deductive <br>verification, first order logic reasoning--, our recent development of Qbricks enables <br>formal specification -- circuit well-formedness, functional behavior, complexity -- <br>and verification for quantum programming with ideal qubits. The goal of this post-<br>doctoral position is to extend  this practice to quantum compilation and physical <br>qubits implementations.  Possibilities include, among others, error correction <br>mechanisms in certified quantum code, together with specifications and reasoning <br>technique for certifying its reliability, automatized certified optimizer for quantum <br>circuits, hardware agnostic assembly language together <br>with its compiler, qubit mapping, etc<br><br>Keywords: quantum programming, compilation, optimization, formal verification, deductive <br>verification<br><br><br>=== HOW TO APPLY<br><br>Applications should be sent to <a href="mailto:christophe.char...@cea.fr">christophe.char...@cea.fr</a> as soon as possible <br>(first come, first served) and by early February 2021 at the latest. Candidates <br>should send a CV, a cover letter, a transcript of all their university results, <br>as well as contact information of two references. The  position is expected to <br>start in May 2021.<br><br>Advisors: Christophe Chareton (CEA), Sébastien Bardin (CEA)<br>Contact: <a href="mailto:christophe.chareton@cea.fr">christophe.chareton@cea.fr</a>, <a href="mailto:sebastien.bardin@cea.fr">sebastien.bardin@cea.fr</a><br><br><br>[1] C. Chareton, S. Bardin, F. Bobot, V. Perrelle, and B. Valiron. An Automated <br>Deductive Verification Framework for Circuit-building Quantum Programs. ESOP <br>2021.<br><br><br></div>