​L’ordinateur quantique parfait n’existe pas encore que déjà, bon nombre d’algorithmes sont prêts à y être implémentés. C’est le cas, par exemple, de l’emblématique algorithme de Shor, qui permet de casser n’importe quelle clé de cryptographie en une fraction de seconde. Les chercheurs du List, qui travaillent aussi sur les logiciels quantiques, développent une expertise pour vérifier en amont de leur exécution sur la machine, que ces logiciels feront bien ce que l’on attend d’eux.

Si des méthodes existent pour tester les programmes classiques, elles ne sont pas applicables sur les programmes quantiques. Les chercheurs ont donc mis au point des outils de vérification dérivés de ceux existants, et qui sont fondés sur les « méthodes formelles » bien maitrisées par le List. Réunis dans l’environnement logiciel QBrick, ils permettent de s’assurer qu’un programme quantique s’exécutera comme prévu sur toutes les entrées possibles.

Grâce à QBrick, les chercheurs ont, pour la toute première fois, réussi à certifier la partie quantique d’une implémentation de l’algorithme de Shor, avec une automatisation supérieure à 95%. Ce taux d’automatisation est trois fois supérieur à ceux des autres certifications existant par le monde, et sur un programme six fois plus grand. Ces résultats ont été présentés à la conférence internationale ESOP 2021, et constituent un jalon important vers la conception de méthodes et environnements efficaces de programmation quantique, positionnant le CEA comme acteur national clé du logiciel quantique.