论文标题
SYMQV：量子程序的自动符号验证
symQV: Automated Symbolic Verification of Quantum Programs
论文作者
论文摘要
我们提出SYMQV，这是用于编写和验证量子电路模型中量子计算的符号执行框架。 SymQV可以自动验证量子程序是否符合一阶规范。我们正式引入了符号量子程序模型。这允许在SMT公式中编码验证问题，然后可以使用Delta-Complete决策过程对其进行检查。我们还提出了一种抽象技术来加快验证过程。实验结果表明，抽象通过对24 QUAT（2^24维状态空间）的量子程序的数量级提高了Symqv的可伸缩性。
We present symQV, a symbolic execution framework for writing and verifying quantum computations in the quantum circuit model. symQV can automatically verify that a quantum program complies with a first-order specification. We formally introduce a symbolic quantum program model. This allows to encode the verification problem in an SMT formula, which can then be checked with a delta-complete decision procedure. We also propose an abstraction technique to speed up the verification process. Experimental results show that the abstraction improves symQV's scalability by an order of magnitude to quantum programs with 24 qubits (a 2^24-dimensional state space).
