<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>
</head>
<body dir="ltr">
<div id="divtagdefaultwrapper" style="font-size:12pt;color:#000000;font-family:Calibri,Helvetica,sans-serif;" dir="ltr">
<p></p>
<div>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.
<br>
<br>
<br>
=== OUR GROUP<br>
<br>
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.
<br>
<br>
See our website at https://qbricks.github.io/ for additional information. <br>
<br>
<br>
=== Position#1 (3 years PhD) Probing quantum verification in the NISQ era<br>
<br>
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. <br>
<br>
Keywords: quantum programming, formal verification, NISQ, quantum error correction<br>
<br>
<br>
=== Position#2 (2 years PostDoc)<br>
<br>
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,
<br>
<br>
Keywords: quantum programming, compilation, optimization, formal verification<br>
<br>
<br>
=== HOW TO APPLY<br>
<br>
Applications should be sent to sebastien.bardin@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. <br>
<br>
Advisors: Sébastien Bardin (CEA), Christophe Chareton (CEA)<br>
Contact: sebastien.bardin@cea.fr<br>
<br>
<br>
[1] C. Chareton, S. Bardin, F. Bobot, V. Perrelle, and B. Valiron. An Automated Deductive Verification Framework for Circuit-building Quantum Programs. ESOP 2021.<br>
</div>
<br>
<p></p>
</div>
</body>
</html>