Building Quantum Software with Trustworthiness

Quantum computing holds the potential to outperform classical computing, and quantum software is a crucial component to unlock its power. Unlike classical computing, quantum software is under the threat of both quantum hardware errors and human bugs due to the unintuitiveness of quantum theory. In this talk, I will discuss our effort to build trustworthy quantum computing software by automated formal methods whereas most existing classical techniques fail to transfer at scale to quantum computing. I will present 1) Giallar, a fully automated verification toolkit for quantum compilers to formally prove that the compiler is bug-free; 2) Gleipnir, an error analysis framework for quantum programs that enable scalable and adaptive quantum error analysis through the application of tensor networks; and 3) QSynth, a program synthesis framework for recursive quantum programs. Finally, I will look to the future and highlight potential research directions for building full-stack trustworthy quantum software systems.