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.


翻译:抽象解释、 Hoare 逻辑和不正确( 逆向 Hoare ) 逻辑是计算机程序静态分析的有力技术。 所有这些技术都成功地扩展到量子设置,但基本上平行发展。 在本文中,我们结合量子与程序核查这些技术之间的关系,抽象领域和量子国家的一套主张结构完善。特别是,我们表明,任何完整的量子抽象解释都引出量子Hare逻辑和量子不正确逻辑,两者都是合理和相对完整的。与文献中提议的逻辑不同,引导逻辑系统是前瞻性的,在某些应用中更有用。相反,任何合理和相对完整的量子体逻辑或量子不正确逻辑都引出完整的量子抽象解释。作为一个应用,如果将本地子空间的图象视为断言,我们就能显示不存在任何声音和相对完整的量子Hare逻辑或不正确逻辑。

0
下载
关闭预览

相关内容

Linux导论,Introduction to Linux,96页ppt
专知会员服务
75+阅读 · 2020年7月26日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
89+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
96+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
IEEE ICKG 2022: Call for Papers
机器学习与推荐算法
3+阅读 · 2022年3月30日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
【ICIG2021】Latest News & Announcements of the Plenary Talk1
中国图象图形学学会CSIG
0+阅读 · 2021年11月1日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
0+阅读 · 2022年8月4日
VIP会员
相关VIP内容
Linux导论,Introduction to Linux,96页ppt
专知会员服务
75+阅读 · 2020年7月26日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
89+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
96+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
相关资讯
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
IEEE ICKG 2022: Call for Papers
机器学习与推荐算法
3+阅读 · 2022年3月30日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
【ICIG2021】Latest News & Announcements of the Plenary Talk1
中国图象图形学学会CSIG
0+阅读 · 2021年11月1日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Top
微信扫码咨询专知VIP会员