As quantum computing becomes an emerging reality, designing efficient quantum programming capabilities is becoming more and more important. Particularly, the debugging and validation of quantum programs is of paramount importance, as these programs are by definition hard to test. Static analysis and formal verification methods for quantum programs started to emerge a few years now, yet they often miss hybrid quantum/classical reasoning facilities with, e.g., generic quantum control, classical control and classical computation instructions. In this paper, we lay out the foundations of a framework for the automated formal verification of (full) hybrid quantum programs featuring both classical and quantum control, measurement and hybrid data structures. In particular, we propose: (1) a novel symbolic representation for describing and manipulating sets of hybrid quantum/classical states called Hybrid Path-Sums (HPS); (2) a set of rewriting rules providing a rich mechanism for simplifying and reasoning on these symbolic hybrid states, and (3) a core assertion language to specify equivalence of hybrid quantum programs, the satisfaction of properties on (parts of) hybrid states, and the extraction of probabilistic statements about the program behavior. We prove the correctness of the novel symbolic representation, of its rewriting system and of the specification system. Finally, we propose a full implementation of this framework as a dedicated symbolic execution engine for hybrid programs. We present an evaluation of a set of representative hybrid case-studies from the literature, showcasing the advantage of our approach and its efficiency compared to state-of-the-art solutions.

翻译：随着量子计算逐步成为新兴现实，设计高效的量子编程能力日益重要。尤其量子程序的调试与验证至关重要，因为这些程序本质上难以测试。尽管量子程序的静态分析与形式化验证方法近年来已开始出现，但它们往往缺乏混合量子/经典推理机制，例如通用量子控制、经典控制及经典计算指令。本文为（全）混合量子程序（同时包含经典控制、量子控制、测量及混合数据结构）的自动化形式化验证奠定框架基础。具体而言，我们提出：（1）一种新型符号表示方法——混合路径求和（Hybrid Path-Sums, HPS），用于描述和操作混合量子/经典状态集合；（2）一组重写规则，提供丰富的机制以简化并推理这些符号化混合状态；（3）核心断言语言，用于规范混合量子程序的等价性、混合状态中（部分）属性的满足性，以及提取程序行为的概率性陈述。我们证明了新型符号表示、重写系统及规范系统的正确性。最后，我们提出该框架的完整实现，作为混合程序的专用符号执行引擎。通过来自文献的一系列代表性混合案例研究评估，展示了我们方法的优势及其相较于当前最优解决方案的高效性。