Title: Toward Automatic Verification of Quantum Programs
Speaker: Mingsheng Ying, UTS
Time/Location: 2-3pm, 9 March 2016 (Wed) / CB11.06.408, FEIT Seminar Room
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.
1. Partial correctness: for any input satisfying the precondition, if the program terminates, then the output satisfies the postcondition.
2. Total correctness: for any input satisfying the precondition, the program terminates and the output satisfies the postcondition.