Abstract interpreters are complex pieces of software: even if the abstract interpretation theory and companion algorithms are well understood, their implementations are subject to bugs, that might question the soundness of their computations. While some formally verified abstract interpreters have been written in the past, writing and understanding them requires expertise in the use of proof assistants, and requires a non-trivial amount of interactive proofs. This paper presents a formally verified abstract interpreter fully programmed and proved correct in the F* verified programming environment. Thanks to F* refinement types and SMT prover capabilities we demonstrate a substantial saving in proof effort compared to previous works based on interactive proof assistants. Almost all the code of our implementation, proofs included, written in a functional style, are presented directly in the paper.


翻译:抽象口译员是复杂的软件:即使抽象解释理论和配套算法得到很好的理解,其实施也会受到错误的影响,这可能对其计算是否正确产生疑问;虽然一些经过正式核实的抽象口译员过去曾写过,但撰写和理解这些解释员需要使用证明助理的专门知识,需要非三重的交互式证明,本文提供了经过正式核实的抽象口译员,在经过核实的F*编程环境中,经过充分编程并证明是正确的。由于F*精细类型和SMT证明能力,我们证明与以前基于互动证据助理的工程相比,在取证工作方面节省了大量费用。几乎所有执行守则,包括以功能风格书写的证据,都直接在文件中提出。

0
下载
关闭预览

相关内容

IFIP TC13 Conference on Human-Computer Interaction是人机交互领域的研究者和实践者展示其工作的重要平台。多年来,这些会议吸引了来自几个国家和文化的研究人员。官网链接:http://interact2019.org/
专知会员服务
61+阅读 · 2021年6月22日
迁移学习简明教程,11页ppt
专知会员服务
107+阅读 · 2020年8月4日
神经常微分方程教程,50页ppt,A brief tutorial on Neural ODEs
专知会员服务
71+阅读 · 2020年8月2日
Python图像处理,366页pdf,Image Operators Image Processing in Python
《可解释的机器学习-interpretable-ml》238页pdf
专知会员服务
201+阅读 · 2020年2月24日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
计算机 | 国际会议信息5条
Call4Papers
3+阅读 · 2019年7月3日
计算机 | 中低难度国际会议信息8条
Call4Papers
9+阅读 · 2019年6月19日
计算机 | ICDE 2020等国际会议信息8条
Call4Papers
3+阅读 · 2019年5月24日
学会期刊丨《中国人工智能学会通讯》2019年 第9卷 第04期
中国人工智能学会
6+阅读 · 2019年4月30日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
人工智能 | 国际会议信息6条
Call4Papers
4+阅读 · 2019年1月4日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
人工智能 | PRICAI 2019等国际会议信息9条
Call4Papers
6+阅读 · 2018年12月13日
计算机 | CCF推荐会议信息10条
Call4Papers
5+阅读 · 2018年10月18日
人工智能 | 国际会议/SCI期刊约稿信息9条
Call4Papers
3+阅读 · 2018年1月12日
Arxiv
0+阅读 · 2021年12月13日
Arxiv
0+阅读 · 2021年12月8日
Arxiv
0+阅读 · 2021年12月6日
Arxiv
7+阅读 · 2021年10月12日
Arxiv
3+阅读 · 2017年12月23日
VIP会员
相关VIP内容
专知会员服务
61+阅读 · 2021年6月22日
迁移学习简明教程,11页ppt
专知会员服务
107+阅读 · 2020年8月4日
神经常微分方程教程,50页ppt,A brief tutorial on Neural ODEs
专知会员服务
71+阅读 · 2020年8月2日
Python图像处理,366页pdf,Image Operators Image Processing in Python
《可解释的机器学习-interpretable-ml》238页pdf
专知会员服务
201+阅读 · 2020年2月24日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
相关资讯
计算机 | 国际会议信息5条
Call4Papers
3+阅读 · 2019年7月3日
计算机 | 中低难度国际会议信息8条
Call4Papers
9+阅读 · 2019年6月19日
计算机 | ICDE 2020等国际会议信息8条
Call4Papers
3+阅读 · 2019年5月24日
学会期刊丨《中国人工智能学会通讯》2019年 第9卷 第04期
中国人工智能学会
6+阅读 · 2019年4月30日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
人工智能 | 国际会议信息6条
Call4Papers
4+阅读 · 2019年1月4日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
人工智能 | PRICAI 2019等国际会议信息9条
Call4Papers
6+阅读 · 2018年12月13日
计算机 | CCF推荐会议信息10条
Call4Papers
5+阅读 · 2018年10月18日
人工智能 | 国际会议/SCI期刊约稿信息9条
Call4Papers
3+阅读 · 2018年1月12日
Top
微信扫码咨询专知VIP会员