Colloquium Details
Toward Automatic Verification of Quantum Programs
| Author: | Mingsheng Ying University of Technology Sydney, Australia and Tsinghua University, China |
|---|---|
| Date: | April 12, 2016 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
Abstract
Programming is error-prone. It is even worse when programming a quantum computer or designing quantum communication protocols, because human intuition is much better adapted to the classical world than to the quantum world?
How can we build automatic tools for verifying correctness of quantum programs and quantum communication protocols?
A logic for verification of both partial correctness and total correctness of quantum programs was developed in our paper [TOPLAS'2011, art. no. 19]. The (relative) completeness of this logic was proved.
Recently, a theorem prover for automatic verification of partial correctness of quantum programs was built based on our logic [arXiv: 1601.03835].
To further develop automatic tools for verifying total correctness of quantum programs, we are working on techniques for synthesis of ranking functions that guarantee termination of quantum programs.
Biography
Mingsheng Ying is a Distinguished Professor with and the Research Director of the Center for Quantum Computation and Intelligent Systems (QCIS), Faculty of Engineering and Information Technology, University of Technology Sydney, Australia, and Cheung Kong Professor with the State Key Laboratory of Intelligent Technology and Systems, Department of Computer Science and Technology, Tsinghua University, Beijing, China.
Ying's research interests are quantum computation, programming theory, and foundations of artificial intelligence. He has published more than 100 papers in top international journals and conferences. He is the author of the books "Foundations of Quantum Programming" (Elsevier - Morgan Kaufmann 2016) and "Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs" (Springer-Verlag, 2001).