Vérification formelle pour la compilation de programmes quantiques

Candidater

Lapos;informatique quantique est aujourdapos;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 sapos;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) dapos;un langage de représentation intermédiaire formellement vérifié pour lapos;implémentation tolérantes aux fautes, (2) dapos;outils de raisonnement pour la certification de fonctions de transformations de circuits quantiques et/ou hybrides classiques/quantiques, (3) dapos;outils automatiques de vérification de propriétés sur des relations dapos;équivalence et/ou de proximité entre circuits quantiques.

Master 2 Informatique

Médias associés

fr_FRFR

Contact us

We will reply as soon as possible...