Celestial: A Smart Contracts Verification Framework

Samvid Dharanikota,Suvam Mukherjee,Chandrika Bhardwaj,Aseem Rastogi,Akash Lal

2021 Formal Methods in Computer Aided Design (FMCAD)（2021）

引用 6|浏览20

暂无评分

摘要

We present CELESTIAL, a framework for formally verifying smart contracts written in the Solidity language for the Ethereum blockchain. CELESTIAL allows programmers to write expressive functional specifications for their contracts. It translates the contracts and the specifications to F* to formally verify, against an F* model of the blockchain semantics, that the contracts me...

查看译文

关键词

Solid modeling,Design automation,Computational modeling,Smart contracts,Semantics,Writing,Tools

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要