Modern separation logics allow one to prove rich properties of intricate code, e.g. functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand, automation with dedicated verifiers typically requires sophisticated proof search algorithms that are specific to the given program logic, resulting in limited tool support that makes it difficult to experiment with program logics, e.g. when learning, improving, or comparing them. Proof outline checkers fill this gap. Their input is a program annotated with the most essential proof steps, just like the proof outlines typically presented in papers. The tool then checks automatically that this outline represents a valid proof in the program logic. In this paper, we systematically develop a proof outline checker for the TaDA logic, which reduces the checking to a simpler verification problem, for which automated tools exist. Our approach leads to proof outline checkers that provide substantially more automation than interactive provers, but are much simpler to develop than custom automatic verifiers.


翻译:现代分离逻辑允许一个人证明复杂代码的丰富特性,例如功能正确性和非阻塞同时代码的线性。 但是,这种表达性导致复杂,使得这些逻辑难以应用。 互动理论验证中的人工证明或证明包含大量步骤, 通常带有微妙的侧面条件。 另一方面, 与专门的验证器进行自动化通常需要复杂的、 符合特定程序逻辑的验证搜索算法, 导致工具支持有限, 使得难以实验程序逻辑, 例如学习、 改进或比较程序逻辑。 校对框检查器填补了这一空白。 它们的输入是一个带有最基本证据步骤的附加说明程序, 与通常在纸张中提供的证明大纲一样。 然后工具自动检查这个大纲是否是程序逻辑中的有效证明。 在本文中, 我们系统开发一个用于将检查简化为简单核查问题的测试框架, 自动工具存在。 我们的方法导致验证大纲检查器比交互式验证器更自动化, 但比定制自动验证器简单得多。

0
下载
关闭预览

相关内容

Automator是苹果公司为他们的Mac OS X系统开发的一款软件。 只要通过点击拖拽鼠标等操作就可以将一系列动作组合成一个工作流,从而帮助你自动的(可重复的)完成一些复杂的工作。Automator还能横跨很多不同种类的程序,包括:查找器、Safari网络浏览器、iCal、地址簿或者其他的一些程序。它还能和一些第三方的程序一起工作,如微软的Office、Adobe公司的Photoshop或者Pixelmator等。
【ACMMM2020】小规模行人检测的自模拟学习
专知会员服务
13+阅读 · 2020年9月25日
专知会员服务
123+阅读 · 2020年9月8日
专知会员服务
39+阅读 · 2020年9月6日
FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
28+阅读 · 2019年10月18日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
58+阅读 · 2019年10月17日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
carla 学习笔记
CreateAMind
9+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
【推荐】图像分类必读开创性论文汇总
机器学习研究会
14+阅读 · 2017年8月15日
Arxiv
0+阅读 · 2021年10月9日
Arxiv
0+阅读 · 2021年10月9日
Arxiv
0+阅读 · 2021年10月8日
The Measure of Intelligence
Arxiv
6+阅读 · 2019年11月5日
Logically-Constrained Reinforcement Learning
Arxiv
3+阅读 · 2018年12月6日
Embedding Logical Queries on Knowledge Graphs
Arxiv
5+阅读 · 2018年9月6日
VIP会员
相关VIP内容
【ACMMM2020】小规模行人检测的自模拟学习
专知会员服务
13+阅读 · 2020年9月25日
专知会员服务
123+阅读 · 2020年9月8日
专知会员服务
39+阅读 · 2020年9月6日
FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
28+阅读 · 2019年10月18日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
58+阅读 · 2019年10月17日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
相关资讯
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
carla 学习笔记
CreateAMind
9+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
【推荐】图像分类必读开创性论文汇总
机器学习研究会
14+阅读 · 2017年8月15日
相关论文
Arxiv
0+阅读 · 2021年10月9日
Arxiv
0+阅读 · 2021年10月9日
Arxiv
0+阅读 · 2021年10月8日
The Measure of Intelligence
Arxiv
6+阅读 · 2019年11月5日
Logically-Constrained Reinforcement Learning
Arxiv
3+阅读 · 2018年12月6日
Embedding Logical Queries on Knowledge Graphs
Arxiv
5+阅读 · 2018年9月6日
Top
微信扫码咨询专知VIP会员