Speeding innovation for industry
Although the perfect quantum computer hasn't been invented yet, algorithms have been developed and are ready to be implemented on tomorrow's quantum machines. The best-known example is probably Shor's algorithm, which can crack virtually any encryption key in a fraction of a second. CEA-List quantum software researchers are studying how to verify during development that quantum programs can be run on a machine and that they will operate as intended.
Verification methods do exist for classical software but are not applicable to quantum programs. CEA-List possesses strong expertise in formal verification methods for classical software, and the quantum verification tools developed here were adapted from these methods. The result is a software environment called QBrick that can be used to verify that a quantum program will run as intended, regardless of the inputs.
In this research, QBrick was used to verify the quantum part of a Shor's algorithm implementation—a world first. And the verification process was more than 95% automated: three times more automation than other verification methods on a program six times the size. The research, which marks a major step toward the development of efficient quantum programming methods and environments and positions the CEA as one of France's leaders in quantum, was presented at ESOP 2021.
CEA is a French government-funded technological research organisation in four main areas: low-carbon energies, defense and security, information technologies and health technologies. A prominent player in the European Research Area, it is involved in setting up collaborative projects with many partners around the world.