论文标题
量子程序的抽象解释，hoare逻辑和错误逻辑
Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
论文作者
论文摘要
抽象的解释，Hoare逻辑和错误（或反向Hoare）逻辑是计算机程序静态分析的强大技术。它们都成功地扩展到量子设置，但在很大程度上并行开发。在本文中，我们在验证量子图的背景下研究了这些技术之间的关系，其中抽象域和量子状态的一组断言是结构良好的。特别是，我们表明，任何完整的量子抽象解释都会诱导量子hoare逻辑和量子不正确的逻辑，它们都是声音且相对完整的。与文献中提出的逻辑不同，诱导的逻辑系统以前瞻性方式，使它们在某些应用程序中更有用。相反，任何声音和相对完整的量子hoare逻辑或量子不正确逻辑都会引起完整的量子抽象解释。作为应用程序，如果将本地子空间的元素作为断言，我们能够显示任何声音和相对完整的量子hoare逻辑或不正确的逻辑的不存在。
Abstract interpretation, Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. All of them have been successfully extended to the quantum setting, but largely developed in parallel. In this paper, we examine the relationship between these techniques in the context of verifying quantum while-programs, where the abstract domain and the set of assertions for quantum states are well-structured. In particular, we show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic, both of which are sound and relatively complete. Unlike the logics proposed in the literature, the induced logic systems are in a forward manner, making them more useful in certain applications. Conversely, any sound and relatively complete quantum Hoare logic or quantum incorrectness logic induces a complete quantum abstract interpretation. As an application, we are able to show the non-existence of any sound and relatively complete quantum Hoare logic or incorrectness logic if tuples of local subspaces are taken as assertions.
