Toward automatic verification of quantum programs. Ying, M. Formal Aspects of Computing, 31(1):3–25, February, 2019.
Paper doi abstract bibtex This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.
@article{ying_toward_2019,
title = {Toward automatic verification of quantum programs},
volume = {31},
issn = {1433-299X},
url = {https://doi.org/10.1007/s00165-018-0465-3},
doi = {10.1007/s00165-018-0465-3},
abstract = {This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.},
language = {en},
number = {1},
urldate = {2022-07-19},
journal = {Formal Aspects of Computing},
author = {Ying, Mingsheng},
month = feb,
year = {2019},
keywords = {Auxiliary rules, Hoare logic, Invariant generation, Proof outline, Quantum programming, Termination analysis},
pages = {3--25},
}
Downloads: 0
{"_id":"uvZierp26KXt5GHCY","bibbaseid":"ying-towardautomaticverificationofquantumprograms-2019","author_short":["Ying, M."],"bibdata":{"bibtype":"article","type":"article","title":"Toward automatic verification of quantum programs","volume":"31","issn":"1433-299X","url":"https://doi.org/10.1007/s00165-018-0465-3","doi":"10.1007/s00165-018-0465-3","abstract":"This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.","language":"en","number":"1","urldate":"2022-07-19","journal":"Formal Aspects of Computing","author":[{"propositions":[],"lastnames":["Ying"],"firstnames":["Mingsheng"],"suffixes":[]}],"month":"February","year":"2019","keywords":"Auxiliary rules, Hoare logic, Invariant generation, Proof outline, Quantum programming, Termination analysis","pages":"3–25","bibtex":"@article{ying_toward_2019,\n\ttitle = {Toward automatic verification of quantum programs},\n\tvolume = {31},\n\tissn = {1433-299X},\n\turl = {https://doi.org/10.1007/s00165-018-0465-3},\n\tdoi = {10.1007/s00165-018-0465-3},\n\tabstract = {This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.},\n\tlanguage = {en},\n\tnumber = {1},\n\turldate = {2022-07-19},\n\tjournal = {Formal Aspects of Computing},\n\tauthor = {Ying, Mingsheng},\n\tmonth = feb,\n\tyear = {2019},\n\tkeywords = {Auxiliary rules, Hoare logic, Invariant generation, Proof outline, Quantum programming, Termination analysis},\n\tpages = {3--25},\n}\n\n","author_short":["Ying, M."],"key":"ying_toward_2019","id":"ying_toward_2019","bibbaseid":"ying-towardautomaticverificationofquantumprograms-2019","role":"author","urls":{"Paper":"https://doi.org/10.1007/s00165-018-0465-3"},"keyword":["Auxiliary rules","Hoare logic","Invariant generation","Proof outline","Quantum programming","Termination analysis"],"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"https://api.zotero.org/groups/4680671/items?key=y3J9nSpB3RsHMnT3bHxi7dHU&format=bibtex&limit=100","dataSources":["MbqeeC74KZhwBpe8j"],"keywords":["auxiliary rules","hoare logic","invariant generation","proof outline","quantum programming","termination analysis"],"search_terms":["toward","automatic","verification","quantum","programs","ying"],"title":"Toward automatic verification of quantum programs","year":2019}