A formally certified end-to-end implementation of Shor's factorization algorithm.

ABSTRACT: Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but it is useful only if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors-"bugs." Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. With such methods, a programmer writes a mathematical specification alongside the program and semiautomatically proves the program correct with respect to it. The proof's validity

SUBMITTER: Peng Y 

PROVIDER: S-EPMC10214188 | biostudies-literature | 2023 May

REPOSITORIES: biostudies-literature