|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Verification of Quantum Programs
If you have a question about this talk, please contact Sergii Strelchuk.
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 termination analysis) of quantum programs.
This talk is part of the CQIF Seminar series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsCambridge Cell Biology Seminar Series Cambridge Neuroscience Symposium - Ion Channels in Health and Disease Engineering for the Life Sciences Seminars
Other talksThe role of pragmatic literacy in estate management Talk by Managing Director of Abellio Greater Anglia Atypical late-time singular regimes accurately diagnosed in stagnation-point-type solutions of 3D Euler flows Buoyancy and chemical effects in geophysics Book launch: The Horn of Africa, State Formation and Decay Rethinking psychosis