@inproceedings{8188eb62a6084b499d1dedf38957f622,
title = "Local Reasoning About Probabilistic Behaviour for Classical–Quantum Programs",
abstract = "Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task greatly. We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour by introducing distribution formulas to specify probabilistic properties. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the effectiveness of the logic, we formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor{\textquoteright}s algorithms.",
keywords = "Hoare logic, Local reasoning, Program verification, Quantum computing, Separation logic",
author = "Yuxin Deng and Huiling Wu and Ming Xu",
note = "Publisher Copyright: {\textcopyright} 2024, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 25th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2024 was co-located with 51st ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2024 ; Conference date: 15-01-2024 Through 16-01-2024",
year = "2024",
doi = "10.1007/978-3-031-50521-8\_8",
language = "英语",
isbn = "9783031505201",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "163--184",
editor = "Rayna Dimitrova and Ori Lahav and Sebastian Wolff",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings",
address = "德国",
}