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.
Read article at https://www.cea-tech.fr/