专栏首页arxiv.org翻译专栏WhylSon:在Why3中证明你的 Michelson 智能合约的重要性(CS PL)
原创

WhylSon:在Why3中证明你的 Michelson 智能合约的重要性(CS PL)

本文介绍了 WhylSon,这是一个用 Michelson 编写的智能合约的推理验证工具,Michelson 是 Tezos 区块链的底层语言。WhylSon 接受正式指定的 Michelson 合约,并自动将其翻译成用 WhyML(Why3 框架的编程和规范语言)编写的等效程序。智能合约的指令被映射到相应的 WhyML 浅层嵌入了它们的公理语义,我们也是在这项工作的背景下开发的。这种方法的一个主要优点是,它允许与 Why3 框架进行开箱即用的集成,即它的 VCGen 和对几个自动定理证明器的后端支持。我们还讨论了使用 WhylSon 来自动证明不同注释的智能合约的正确性。

原文题目:WhylSon: Proving your Michelson Smart Contracts in Why3

原文:This paper introduces WhylSon, a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. WhylSon accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into a corresponding WhyML shallow-embedding of the their axiomatic semantics, which we also developed in the context of this work. One major advantage of this approach is that it allows an out-of-the-box integration with the Why3 framework, namely its VCGen and the backend support for several automated theorem provers. We also discuss the use of WhylSon to automatically prove the correctness of diverse annotated smart contracts.

原文作者:Luís Pedro Arrojado da Horta, João Santos Reis, Mário Pereira, Simão Melo de Sousa

原文地址:https://arxiv.org/abs/2005.14650

原创声明,本文系作者授权云+社区发表,未经许可,不得转载。

如有侵权,请联系 yunjia_community@tencent.com 删除。

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 做数据分析必须学R的4个理由

    R 是一种灵活的编程语言,专为促进探索性数据分析、经典统计学测试和高级图形学而设计。R 拥有丰富的、仍在不断扩大的数据包库,处于统计学、数据分析和数据挖掘发展的...

    华章科技
  • 做数据分析必须学R语言的4个理由

    R 是一种灵活的编程语言,专为促进探索性数据分析、经典统计学测试和高级图形学而设计。R 拥有丰富的、仍在不断扩大的数据包库,处于统计学、数据分析和数据挖掘发展的...

    小莹莹
  • 做数据分析必须学R的4个理由

    R 是一种灵活的编程语言,专为促进探索性数据分析、经典统计学测试和高级图形学而设计。R 拥有丰富的、仍在不断扩大的数据包库,处于统计学、数据分析和数据挖掘发展的...

    小莹莹
  • 收藏贴 :2019年必备43种区块链开发工具 原

    本文列出2019年最新整理的用于区块链开发的43种流行的开发库、开发工具与开发框架。

    用户1408045
  • FPGA系统性学习笔记连载_Day5 Xilinx ZYNQ7000系列基本开发流程之PL端篇

    本系列为FPGA系统性学习学员学习笔记整理分享,如有学习或者购买开发板意向,可加交流群联系群主。

    FPGA技术江湖
  • 【技术干货】kube-scheduler里的调度框架

    本文主要介绍k8s.io/kubernetes/pkg/scheduler/framework的调度流程。

    CNCF
  • 要玩转这个星际争霸II开源AI,你只需要i5+GTX1050

    Reaver 是一个模块化的深度强化学习框架,可提供比大多数开源解决方案更快的单机并行化能力,支持星际争霸 2、OpenAI Gym、Atari、MuJoCo ...

    机器之心
  • 告诉你做数据分析必须学R的4个理由

    论坛君:你很可能已经听说过 R,或许你知道 R 是一种编程语言,而且知道它与统计学有关,但它是否适合您呢?本文作者将试图向大家讲解他对R的看法,分享他认为试用开...

    小莹莹
  • PHP 到底是不是宇宙第一?TIOBE 排行榜来证明!

    做为一名程序员,都比较关注其使用编程语言的热度,一方面编程语言的热度决定了它拥有多大的市场,另一方面也关系到行业内程序员选择机会有多大。

    用户6543014
  • PHP 到底是不是宇宙第一?TIOBE 排行榜来证明!

    做为一名程序员,都比较关注其使用编程语言的热度,一方面编程语言的热度决定了它拥有多大的市场,另一方面也关系到行业内程序员选择机会有多大。

    纯洁的微笑
  • PL-VINS:实时基于点线的单目惯导SLAM系统

    标题:PL-VINS: Real-Time Monocular Visual-Inertial SLAM with Point and Line

    点云PCL博主
  • 史上最快AI计算机发布!谷歌TPU V3的1/5功耗、1/30体积,首台实体机已交付

    这个名为Cerebras Wafer Scale Engine(WSE)的“巨无霸”面积达到42225 平方毫米,拥有1.2 万亿个晶体管,400000 个核心...

    大数据文摘
  • 动态 | 由 AI 芯片到目标检测板,「西安交大」是如何斩获 DAC FPGA 赛道亚军?

    AI 科技评论按:2019 年 6 月 5 日,由电子自动化设计顶级会议 DAC 2019 主办的「低功耗目标检测系统设计挑战赛」于美国拉斯维加斯落下帷幕。西安...

    AI科技评论
  • 使用方向变换(directional transform)图像分块压缩感知

    论文的思路是先介绍分块压缩感知BCS,然后介绍使用投影和硬阈值方法的迭代投影方法PL,接着将PL与维纳滤波器结合形成SPL(平滑PL),并且介绍了稀疏表示的几种...

    闪电gogogo
  • 10.深入k8s:调度的优先级及抢占机制源码分析

    上一篇我们将了获取node成功的情况,如果是一个优先pod获取node失败,那么就会进入到抢占环节中,那么抢占环节k8s会做什么呢,抢占是如何发生的,哪些资源会...

    luozhiyun
  • 一文读懂常用开源许可证

    社区时常为流行产品中有争议的开源许可证而感到震惊,这引起各方关注,纷纷争论何为真正的开源许可证。去年,Apache 基金会(Apache Foundation)...

    心莱科技雪雁
  • 分布式系统理论基础6:Raft、Zab

    本文转自:https://www.cnblogs.com/bangerlee/p/5991417.html

    Java技术江湖
  • 更大意味着更好吗?Cerebras史上最强深度学习计算机诞生始末

    如今,时间刚过去1个多月,在洛斯阿尔托斯的Cerebras总部,一些客户已经通过光纤电缆将他们的数据输入了4台CS-1计算机进行训练,这些64厘米高的机器不停地...

    大数据文摘
  • 西安交大获得DAC19系统设计竞赛FPGA赛道亚军,这里是他们的设计方案

    2019 年 6 月 5 日,由自动化设计顶级会议 Design Automation Conference(DAC'2019, CCF A 类会议)主办的第二...

    机器之心

扫码关注云+社区

领取腾讯云代金券