Quantum Programming

Refinement calculus of quantum programs with projective assertions
This paper presents a refinement calculus designed specifically for quantum programs, offering a structured approach to their …
Yuan Feng, Li Zhou, Yingte Xu, Xiaoquan Xu
引用 DOI URL
Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
Abstract interpretation, Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of …
Yuan Feng, Sanjiang Li
引用 DOI URL
Verification of Nondeterministic Quantum Programs
Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the …
Yuan Feng, Yingte Xu
引用 DOI URL
Verification of Distributed Quantum Programs
Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of …
Yuan Feng, Sanjiang Li, Mingsheng Ying
引用 DOI URL
A proof system for disjoint parallel quantum programs
In this paper, we define the operational and denotational semantics of a special class of parallel quantum programs, namely disjoint …
Mingsheng Ying, Li Zhou, Yangjia Li, Yuan Feng
引用 DOI URL
Projection-based runtime assertions for testing and debugging Quantum programs
In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The …
Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, Yuan Xie
引用 DOI URL
Quantitative robustness analysis of quantum programs
Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major …
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, Xiaodi Wu
引用 DOI URL
Reachability analysis of quantum Markov decision processes
We introduce the notion of quantum Markov decision process (qMDP) as a semantic model of nondeterministic and concurrent quantum …
Shenggang Ying, Mingsheng Ying
引用 DOI URL
Algorithmic analysis of termination problems for quantum programs
We introduce the notion of linear ranking super-martingale (LRSM) for quantum programs (with nondeterministic choices, namely angelic …
Yangjia Li, Mingsheng Ying
引用 DOI URL
Invariants of quantum programs: characterisations and generation
Program invariant is a fundamental notion widely used in program verification and analysis. The aim of this paper is twofold: (i) find …
Mingsheng Ying, Shenggang Ying, Xiaodi Wu
引用 DOI URL