Logic List Mailing Archive

CfA: 3 postdoctorial position quantum programming / program analysis / formal methods, Paris (France), deadline: asap

The  quantum software group @ CEA List, Universit Paris-Saclay, offers t
hree years fully-funded postdoctoral 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 quan
tum programs, integrated in the Software Safety Laboratory of CEA List, Uni
versit? Paris-Saclay. Our long term goal is to design and develop formal te
chniques and tools enabling productive and certified quantum programming. E
specially, we develop Qbricks [1,2], a proof of concept environment for for
mally verified quantum programming language.

See our website at https://qbricks.github.io/ for additional information, d
etails for the position at https://github.com/Qbricks/qbricks.github.io/fil
es/15310776/Fiche_de_poste_postdoc_qbricks.pdf.

=== ABOUT THE POSTDOC POSITION

We consider the standard quantum hybrid model, where a classical program bu
ilds a quantum circuit and sends it to a quantum co-processor. In these pos
itions, we are interested in verification mechanisms aiming at ensuring tha
t a quantum program implementation indeed satisfies its intended behaviour.
 Possibilities include, among others, ? high-level automatic verification o
f quantum programs for implicit program properties, ? design of verificatio
n oriented hybrid quantum programming languages ? high-level functional rea
soning for quantum programs, ? circuit-level automatic verification of quan
tum programs, ? verification of circuit transformation and compilation.


Keywords: quantum programming, compilation, formal verification, deductive
verification


=== HOW TO APPLY

Applications should be sent to christophe.char...@cea.fr as soon as possibl
e (first come, first served). Candidates should send a CV, a cover letter, 
a transcript of all their university results,
as well as contact information of two references. The  position is expected
 to start in October 2024.

Advisors: Christophe Chareton (CEA), S?bastien Bardin (CEA)
Contact: christophe.chareton@cea.fr, sebastien.bardin@cea.fr


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

[2] Christophe Chareton, Dongho Lee, Beno?t Valiron, Renaud Vilmart, S?bast
ien Bardin, Zhaowei Xu: Formal Methods for Quantum Algorithms. Handb. Forma
l Anal. Verification Cryptogr. 2023: 319-422
--
[LOGIC] mailing list, provided by DLMPST
More information (including information about subscription management) can
be found here: http://dlmpst.org/pages/logic-list.php