Malfunctions in software like airplane control systems or nuclear plant control systems can have catastrophic consequences. Formal verification is the only form of sofware testing that can guarantee the absence of bugs. Formally verified software gives a mathematical proof that the specification is correctly implemented and that no bugs would induce unwanted behaviour. This has a high development cost and having an entirely verified program takes time and effort. However, having verified components already has great benefits. We implement in Scala and formally verify with Stainless a hash map that can then be reused and act as a basis on which to rely. The implementation we propose is based on the LongMap of the Scala standard library with some minor adaptations. This map is implemented with mutable arrays. We give the specification with respect to an implementation of a map based on a list of tuples, that we implement and formally verify as well.


翻译:象飞机控制系统或核电站控制系统这样的软件的功能失灵可能产生灾难性后果。 正式核查是能够保证没有错误的唯一软体测试形式。 正式核查的软件提供了一个数学证据, 证明规格得到正确执行, 没有错误会引起不想要的行为。 开发成本高, 程序经过完全核查需要时间和精力。 但是, 已经核实的部件已经有很大的好处 。 我们在Scala 执行一张可以再利用的散列地图, 并与Stainless 一起正式核查, 并以此为依据。 我们提议的执行以Scala 标准库长映射为基础, 并进行一些小的修改 。 该地图是用变形阵列执行的。 我们给出执行地图的规格, 以图具清单为基础, 我们执行并正式核实地图 。

0
下载
关闭预览

相关内容

Scala 是一门现代的多范式编程语言,志在以简练、优雅及类型安全的方式来表达常用编程模式。它平滑地集成了面向对象和函数语言的特性。Scala 运行于Java 平台(Java 虚拟机),并兼容现有的 Java 程序。
【干货书】开放数据结构,Open Data Structures,337页pdf
专知会员服务
16+阅读 · 2021年9月17日
【Manning新书】C++并行实战,592页pdf,C++ Concurrency in Action
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
CCF C类 | DSAA 2019 诚邀稿件
Call4Papers
6+阅读 · 2019年5月13日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
美国化学会 (ACS) 北京代表处招聘
知社学术圈
11+阅读 · 2018年9月4日
计算机类 | 期刊专刊截稿信息9条
Call4Papers
4+阅读 · 2018年1月26日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
强化学习 cartpole_a3c
CreateAMind
9+阅读 · 2017年7月21日
Arxiv
0+阅读 · 2021年9月17日
Arxiv
0+阅读 · 2021年9月16日
The Measure of Intelligence
Arxiv
6+阅读 · 2019年11月5日
VIP会员
相关VIP内容
相关资讯
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
CCF C类 | DSAA 2019 诚邀稿件
Call4Papers
6+阅读 · 2019年5月13日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
美国化学会 (ACS) 北京代表处招聘
知社学术圈
11+阅读 · 2018年9月4日
计算机类 | 期刊专刊截稿信息9条
Call4Papers
4+阅读 · 2018年1月26日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
强化学习 cartpole_a3c
CreateAMind
9+阅读 · 2017年7月21日
Top
微信扫码咨询专知VIP会员