A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL(2022)
摘要
It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space explosion problem for quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we are able to infuse separation logic into our framework and apply local reasoning using a quantum frame rule that is similar to the classical frame rule. For evaluation, we apply our framework to verify various quantum programs including DeutschsJozsa's algorithm and Grover's algorithm.
更多查看译文
关键词
Quantum Computing, Verification, Formal Semantics
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要