About us
Espace utilisateur
Education
INSTN offers more than 40 diplomas from operator level to post-graduate degree level. 30% of our students are international students.
Professionnal development
Professionnal development
Find a training course
INSTN delivers off-the-self or tailor-made training courses to support the operational excellence of your talents.
Human capital solutions
At INSTN, we are committed to providing our partners with the best human capital solutions to develop and deliver safe & sustainable projects.
Thesis
Home   /   Thesis   /   Formal verification for quantum programs compilation

Formal verification for quantum programs compilation

Computer science and software Engineering sciences New computing paradigms, circuits and technologies, incl. quantum Technological challenges

Abstract

While recent progress in quantum hardware open the door for significant speedup in cryptography as well as additional key areas (biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge.

Adapting the best practice for classical computing formal verification -- deductive verification, first order logic reasoning--, our recent development of Qbricks enables formal specification -- circuit well-formedness, functional behavior, complexity --and verification for quantum programming with ideal qubits.

The goal of PhD position is to extend this practice into the quantum compilation chain by making it usable from mainstream quantum programming environments (high-level programming and imperative paradigm).

Possibilities include, among others, developing (1) a formally verified intermediate representation for fault-tolerant implementations (2) reasoning tools for certifying quantum circuit transformation functions, (3) automatic verification tools over equivalence and/or proximity relations between quantum circuits.

Laboratory

Département Ingénierie Logiciels et Systèmes (LIST)
LSL (DILS)
Laboratoire pour la Sûreté du Logiciel
Université de Lorraine
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down