Automated Smart Contract Synthesis and Verification for Distributed Ledger Blockchain Technology

比特币！以太！区块链！密码经济学！在过去的一年里，这些话成了头条新闻 全球范围内。基于分布式分类账的技术(DLT)--也被称为“价值互联网”--的前景已经实现 并创造了上一次在20世纪90年代出现的对技术的兴奋 当互联网进入主流的时候。可能的广泛采用和 完全分散的治理承诺的基本技术哲学 撼动商业、金融和隐私/安全等领域。从2016年以来的投资流入来看(比任何其他科技行业都要大)，它有望重新定义 全球和剧烈规模的社会的社会经济结构。这个 这些技术的发展几乎完全发生在主流之外 科技行业由个人推动，自称“赛博朋克”。 大学和他们的研究人员在很大程度上一直处于观望状态。和 这是一个令人担忧的问题。因此，至关重要的是，这些创新必须以健全的技术原则为基础，从而实现善政和 社会进步。DLT的一个主要优势是称为智能合同的软件的分布式部署，这提供了一系列全新的机会。例如，它允许分散的商业、分散的证券交易、分散的金融衍生证券、完全自动化的供应链管理，或自动执行和转让艺术家的财产权。作为数百万美元的资产或房地产契约登记在 区块链是由这种软件处理的，攻击或操纵它变得有利可图，正如最近的DAO和奇偶钱包攻击在过去两年中已经证明的那样，智能合同软件中的错误(错误)造成了超过2.5亿美元的损失。该项目旨在通过以下方式弥合这一差距：(A)开发一种新的编程语言，该语言包含高效编写智能合同所需的最常见操作；(B)为该语言建立一个全面的验证环境，以帮助检查正确性，即使在新手软件工程师的层面上也是如此；(C)为智能合同生成软件开发基于模板的自动合成工具，该软件在设计上是正确的；以及(D)使用所提出的生态系统来沙箱分散的先知(其目的是将现实生活中的信息输入到区块链上)，以展示大规模研究的有效性和实用性。

Bitcoin! Ethereum! Blockchain! Crypto-economics! In the past year, these words made headline news globally. The promise of Distributed Ledger-based Technologies (DLT) - also known as the "internet of value"- has electrified the world and created an excitement for technology that was last seen in the 1990s when the internet was entering mainstream. The possible widespread adoption and underlying technological philosophy of fully decentralized governance promises to shake up the worlds of commerce, finance, and privacy/security, among others. Judging from the investment inflows since 2016 (larger than any other technology sector), it promises redefine the socioeconomic fabric of society at a global and drastic scale. The development of these technologies occurred almost entirely occurred outside of the mainstream tech sector advanced by individuals, self-declared “cypherpunks.” Universities and their researchers have been largely at the sidelines. And that's a concern. As such, it is critical that these innovations are based on sound technological principles that enable good governance and societal progress. One major advantage of DLT is the distributed deployment of software called smart contracts which present a whole new set of opportunities. For example, it allows decentralized commerce, decentralized trading of securities, decentralized financial derivative securities, fully automated supply-chain management, or automatic enforcement and transfers of artists' property rights. As multi-million dollar assets or real estate deeds registered on a blockchain are handled by this software, attacking or manipulating it becomes lucrative, as the recent DAO and Parity wallet attacks already demonstrated in the past two years with more than $250 million dollars lost due to errors (bugs) in smart contract software. This projects aims to bridge this gap by: (a) developing a novel programming language that comprises the most common operations needed to code smart contracts efficiently; (b) building a comprehensive verification environment for this language to assist checking correctness even at the level of a novice software engineer; (c) developing a template-based automated synthesis tool for smart contracts generating software that is "correct by design" and (d) using the proposed ecosystem to sandbox a decentralized oracle (whose purpose is to input real life information onto the blockchain) so as to demonstrate the efficacy and practicality of the research on a large scale.