As quantum computing is rising in popularity, the amount of quantum programs and the number of developers writing them are increasing rapidly. Unfortunately, writing correct quantum programs is challenging due to various subtle rules developers need to be aware of. Empirical studies show that 40-82% of all bugs in quantum software are specific to the quantum domain. Yet, existing static bug detection frameworks are mostly unaware of quantum-specific concepts, such as circuits, gates, and qubits, and hence miss many bugs. This paper presents LintQ, a comprehensive static analysis framework for detecting bugs in quantum programs. Our approach is enabled by a set of abstractions designed to reason about common concepts in quantum computing without referring to the details of the underlying quantum computing platform. Built on top of these abstractions, LintQ offers an extensible set of ten analyses that detect likely bugs, such as operating on corrupted quantum states, redundant measurements, and incorrect compositions of sub-circuits. We apply the approach to a newly collected dataset of 7,568 real-world Qiskit-based quantum programs, showing that LintQ effectively identifies various programming problems, with a precision of 91.0% in its default configuration with the six best performing analyses. Comparing to a general-purpose linter and two existing quantum-aware techniques shows that almost all problems (92.1%) found by LintQ during our evaluation are missed by prior work. LintQ hence takes an important step toward reliable software in the growing field of quantum computing.

翻译：随着量子计算日益普及，量子程序数量及编写此类程序的开发者正快速增长。然而，由于开发者需注意多种细微规则，编写正确的量子程序极具挑战。实证研究表明，量子软件中40%-82%的错误属于量子领域特有缺陷。然而，现有静态错误检测框架大多未考虑量子特定概念（如电路、门和量子比特），因此遗漏了大量错误。本文提出LintQ，这是一个用于检测量子程序错误的综合性静态分析框架。该方法通过设计一组抽象层来实现，这些抽象层能够在无需参考底层量子计算平台细节的情况下，推理量子计算中的常见概念。基于这些抽象层，LintQ提供了可扩展的十项分析功能，用于检测潜在错误，例如操作损坏的量子态、冗余测量以及子电路的不正确组合。我们将该方法应用于新收集的7,568个基于Qiskit的真实量子程序数据集，结果表明LintQ能有效识别各类编程问题，在其默认配置下（六项最佳性能分析）精确率达91.0%。与通用性代码检查工具及两项现有量子感知技术的比较显示，评估期间LintQ发现的几乎所有问题（92.1%）均未被先前工作检出。因此，LintQ在日益发展的量子计算领域中，为迈向可靠软件迈出了重要一步。