Open Collections

Toward automatic verification of quantum programs

Banff International Research Station for Mathematical Innovation and Discovery

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? A logic for verification of both partial correctness and total correctness of quantum programs was developed in our TOPLAS'2011 paper. The (relative) completeness of this logic was proved. Recently, a theorem prover for verification of quantum programs was built based on this logic [arXiv: 1601.03835]. To further develop automatic tools, we are working on techniques for invariant generation and synthesis of ranking functions for quantum programs.

Mathematics; Quantum theory; Information and communication, circuits; Theoretical computer science

video/mp4

Author affiliation: University of Technology Sydney

2016-10-19

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/59506

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/