Même si ce n’est pas encore tout à fait pour demain, les ordinateurs quantiques démultiplieront un jour de façon exponentielle les capacités de calcul dans certains domaines clés. Et les chercheurs se préparent dès maintenant à vérifier que les programmes que l’on y implémentera feront bien ce que l’on attend d’eux, ce qui n’est pas une mince affaire ! Si des méthodes existent pour tester les programmes classiques, elles ne sont pas applicables sur de tels ordinateurs, à la fois trop coûteuses ou impossibles à mettre en œuvre.
Afin de pallier le manque d’outils d’analyse fiables, les chercheurs de l’institut Carnot CEA List ont mis à profit leur forte expertise en sécurité informatique : ils ont utilisé les méthodes formelles, des techniques à l’état de l’art pour vérifier que des programmes classiques ne comportent pas de bugs, afin de les rendre compatibles avec la vérification de code quantique. Après avoir fait évoluer chaque brique logique (spécification des comportements attendus du système, caractérisation mathématique des comportements effectifs du système, et algorithme vérifiant que ces derniers sont conformes aux attentes), ils ont donné naissance à QBrick, un environnement de spécification, programmation et vérification formelle de programmes quantiques, qui repose sur les meilleures pratiques des méthodes formelles pour le cas classique, en les spécifiant au cas quantique. Pour valider cette avancée significative, ils l’ont appliquée à un cas complexe : l’algorithme de phase quantique (QPE), l’élément essentiel de l’algorithme de Shor, lequel permettrait de casser les clés utilisées pour les transactions bancaires. Une première !
Retrouvez cette actualité sur http://www.cea-tech.fr/