PhD Defense: Theoretical and Practical High-Assurance Software Tools for Quantum Applications

Quantum computing promises to transform our approach to solving significant computational challenges, such as factorization and quantum system simulation. Harnessing this quantum power in real life necessitates software stack support. This talk focuses on the critical challenges encountered in the software for quantum computing, aiming to shape high-assurance software stacks for controlling quantum computing devices in the immediate future and beyond. First, I will present software tools we have developed for Hamiltonian-oriented quantum computing, encompassing a pioneering framework for Hamiltonian-oriented programming and a theoretical approach to the differentiation of parameterized quantum systems. Then I will demonstrate the application of formal methods in ensuring quantum software correctness for circuit-oriented quantum computing, including a formally certified implementation of Shor's factorization algorithm and a theoretical framework for algebraically reasoning about the equivalences of quantum while programs. Our work illuminates the path to achieving practical quantum applications in the near term with a high-assurance software stack.