symQV：量子程序的自动化符号验证
量子物理
2023-03-14 v1 计算机科学中的逻辑
摘要
我们提出 symQV，一个用于在量子电路模型中编写和验证量子计算的符号执行框架。symQV 可自动验证量子程序是否符合一阶规范。我们形式化地引入了一种符号量子程序模型。这使得能够将验证问题编码为一个 SMT 公式，随后可用 delta-完全判定过程进行检查。我们还提出了一种抽象技术以加速验证过程。实验结果表明，该抽象将 symQV 对具有 24 个量子比特（一个 2^24 维状态空间）的量子程序的可扩展性提升了一个数量级。
引用
@article{arxiv.2212.02267,
title = {symQV: Automated Symbolic Verification of Quantum Programs},
author = {Fabian Bauer-Marquart and Stefan Leue and Christian Schilling},
journal= {arXiv preprint arXiv:2212.02267},
year = {2023}
}
备注
This is the extended version of a paper with the same title that appeared at FM 2023. Tool available at doi.org/10.5281/zenodo.7400321