Qui sommes-nous ?
Espace utilisateur
Formation continue
Credit : L. Godart/CEA
D’un jour à plusieurs semaines, nos formations permettent une montée en compétence dans votre emploi ou accompagnent vers le retour à l’emploi. 
Conseil et accompagnement
Crédit : vgajic
Fort de plus de 60 ans d’expériences, l’INSTN accompagne les entreprises et organismes à différents stades de leurs projets de développement du capital humain.
Thèses
Accueil   /   Thèses   /   Vérification formelle pour la compilation de programmes quantiques

Vérification formelle pour la compilation de programmes quantiques

Défis technologiques Informatique et logiciels Nouveaux paradigmes de calculs, circuits et technologies, dont le quantique Sciences pour l’ingénieur

Résumé du sujet

L'informatique quantique est aujourd'hui un domaine hautement prometteur, avec des applications décisives dans de nombreux domaines clés (biologie, chimie, cryptographie, optimisation, apprentissage machine, etc).

Un des défis les plus importants dans ce champ émergeant est la validation des programmes.
En s'inspirant des meilleures techniques existantes pour la vérification formelle de programmes classiques -- vérification déductive, raisonnement en logique de premier ordre -- notre récent développement de Qbricks permet la spécification formelle -- bonne formation des circuits, comportement fonctionnel, complexité -- et la vérification de programmes quantiques opérant sur des qubits idéaux.

Le but de cette thèse est d’étendre l’usage de cette pratique dans la chaîne de compilation quantiques.
Les possibilités sont notamment les développement (1) d'un langage de représentation intermédiaire formellement vérifié pour l'implémentation tolérantes aux fautes, (2) d'outils de raisonnement pour la certification de fonctions de transformations de circuits quantiques et/ou hybrides classiques/quantiques, (3) d'outils automatiques de vérification de propriétés sur des relations d'équivalence et/ou de proximité entre circuits quantiques.

Laboratoire

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