Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Toward automatic verification of quantum programs
Ying M. Formal Aspects of Computing31 (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 (2012-0296)
Bookmark and Share
  Editor Recommended
 
 
Information Theory (H.1.1 ... )
 
 
Physics (J.2 ... )
 
 
Verification (D.4.5 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Information Theory": Date
A generalized class of certainty and information measures.
van der Lubbe J., Boekee D. Information Sciences 32(3): 187-215, 1984. Type: Article
Jan 1 1985
Information in the enterprise
Darnton G., Giacoletto S., Digital Press, Newton, MA, 1992. Type: Book (9780131761735)
Sep 1 1993
Information theory for information technologists
Usher M., Macmillan Press Ltd., Basingstoke, UK, 1984. Type: Book (9789780333367032)
Sep 1 1985
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy