Yuan Feng

Title: Hoare logic for verification of quantum programs

Abstract:  Quantum computing and quantum communication provide potential speed-up and enhanced security compared with their classical counterparts. However, the analysis of quantum algorithms and protocols is notoriously difficult. Furthermore, due to the lack of reliable and scalable quantum hardware, traditional techniques such as testing and debugging in classical software engineering will not be readily available in the near future, while static analysis of quantum programs based on formal methods seems indispensable. In this talk, I will introduce Hoare logic, a syntax-oriented method for reasoning about program correctness which has been shown to be effective in the verification of classical and probabilistic programs. An extension of Hoare logic to a simple quantum while-language will be discussed, and some examples will be given to illustrate its utility.

Bio:  Prof. Yuan Feng received his Bachelor of Science and Ph.D. in Computer Science from Tsinghua University, China in 1999 and 2004, respectively. He is currently a professor at the Centre for Quantum Software and Information, University of Technology Sydney (UTS), Australia. Before joining UTS in 2009, he was an associate professor at Tsinghua University. His research interests include quantum information and quantum computation, quantum programming theory, and probabilistic systems. He was awarded an ARC (Australian Research Council) Future Fellowship in 2010.

Contact the speaker: