Program logics typically reason about an over-approximation of program behaviour to prove the absence of bugs. Recently, program logics have been proposed that instead prove the presence of bugs by means of under-approximate reasoning, which has the promise of better scalability. In this paper, we present an under-approximate program logic for a nondeterministic graph programming language, and show how it can be used to reason deductively about program incorrectness, whether defined by the presence of forbidden graph structure or by finitely failing executions. We prove this incorrectness logic to be sound and complete, and speculate on some possible future applications of it.


翻译:程序逻辑通常说明程序行为过度偏好的理由,以证明没有错误。 最近,有人提议程序逻辑,以近似推理来证明存在错误,这有可能改善可缩放性。 在本文中,我们提出了一个非确定性图表编程语言的近似程序逻辑,并表明如何利用它来推算程序不正确性,无论是用被禁止的图表结构来界定,还是用有限的不成功处决来界定。 我们证明这种不正确逻辑是正确和完整的,并推测它今后可能使用的某些用途。

0
下载
关闭预览

相关内容

强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
已删除
将门创投
12+阅读 · 2018年6月25日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
carla 学习笔记
CreateAMind
9+阅读 · 2018年2月7日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
0+阅读 · 2021年7月5日
Arxiv
0+阅读 · 2021年7月2日
Arxiv
0+阅读 · 2021年6月30日
Arxiv
7+阅读 · 2019年6月20日
Logic Rules Powered Knowledge Graph Embedding
Arxiv
7+阅读 · 2019年3月9日
VIP会员
相关主题
相关资讯
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
已删除
将门创投
12+阅读 · 2018年6月25日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
carla 学习笔记
CreateAMind
9+阅读 · 2018年2月7日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
相关论文
Top
微信扫码咨询专知VIP会员