Loading...
Please wait, while we are loading the content...
Similar Documents
Generating Coq Specifications from DeepSEA Specifications of Solidity Contracts
| Content Provider | Semantic Scholar |
|---|---|
| Author | Fu, Christopher D. Shao, Zhong Sjöberg, Vilhelm |
| Copyright Year | 2017 |
| Abstract | Ethereum is a public, open-source platform that allows users to create contracts that can store data on the Ethereum blockchain and send and receive messages to and from other contracts. Such contracts can be combined in complex ways to create powerful decentralized applications. Because of the nature of the Ethereum blockchain, bugs in contract code are difficult to rectify and may lead to large monetary losses if exploited. For this project, we propose to extend the compiler for DeepSEA, a certified programming language used in the development of mCertiKOS, to generate Coq specifications from DeepSEA specifications of Ethereum contracts written in Solidity. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://zoo.cs.yale.edu/classes/cs490/17-18b/fu.christopher.cf449/proposal.pdf |
| Alternate Webpage(s) | https://zoo.cs.yale.edu/classes/cs490/17-18a/fu.christopherdavid.cf449/proposal.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
