Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Best of 2016 Recommended by Editor Recommended by Reviewer Recommended by Reader
Toward automatic verification of quantum programs
Ying M.  Formal Aspects of Computing 31 (1): 3-25, 2019. Type: Article
Date Reviewed: Jul 28 2020

Even if a world of quantum computing for everyone is years (if not decades) away, research on designing proper ways to program such systems has been ongoing for quite some time. History shows that programming is hard; making correct programs, that is, ones that conform to specifications, requires rigor and formal reasoning. Adapting the wide spectrum of formal techniques developed by the (classical) programming language community, from semantics to verification frameworks to proof assistants to the quantum paradigm, is thus key.

Ying’s work, which started years ago, focuses on defining a quantum Hoare-style logic approach to (quantum) program verification. This paper puts together a roadmap for the automatic verification of quantum programs written in a “while”-style idiom, extended to handle Hilbert-space states, unitary operators, and quantum variables. The agenda is actually pretty straightforward: follow all the traditional steps (syntax, operational, and denotational semantics; partial and total correctness; Hoare logic; proof techniques; invariants; mechanization) but with a quantum twist.

Readers need to be well versed in quantum computation notions (density operators, the Hadamard gate, entanglement, the controlled NOT gate (CNOT)) to really appreciate the results. However, even the uninitiated will get a feeling of the complexity induced by quantum specificities over traditional verification techniques. There is much more to be done (in this framework and in other competing approaches to quantum programming), so I would recommend this paper to programming language researchers interested in applying their knowledge to this new world.

Reviewer:  P. Jouvelot Review #: CR147025
Bookmark and Share
  Editor Recommended
Information Theory (H.1.1 ... )
Physics (J.2 ... )
Verification (D.4.5 ... )
Would you recommend this review?
Other reviews under "Information Theory": Date
The theory of quantum information
Watrous J.,  Cambridge University Press, New York, NY, 2018. 598 pp. Type: Book (978-1-107180-56-7)
Nov 21 2019
Universal quantum computing: supervening decoherence -- surmounting uncertainty
Amoroso R.,  World Scientific Publishing Co, Inc., Hackensack, NJ, 2017. 632 pp. Type: Book
May 22 2019
Resilient wireless sensor networks: the case of network coding
Al-Kofahi O., Kamal A.,  Springer International Publishing, New York, NY, 2015. 68 pp. Type: Book (978-3-319239-63-7)
Jul 15 2016

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2020 ThinkLoud, Inc.
Terms of Use
| Privacy Policy