Difference between revisions of "IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain"

From FSL
Jump to: navigation, search
(Created page with "<pubbib id='kasampalis-guth-moore-serbanuta-zhang-filaretti-serbanuta-johnson-rosu-2019-fm' template='PubDefaultWithAbstractAndTitle'/>")
 

Latest revision as of 20:14, 11 July 2019

IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Kasampalis, Theodoros and Guth, Dwight and Moore, Brandon and Serbanuta, Traian Florin and Zhang, Yi and Filaretti, Daniele and Serbanuta, Virgil and Johnson, Ralph and Rosu, Grigore
FM 2019. 2019. To appear
Abstract. This paper proposes IELE, an LLVM-style language, together with a tool ecosystem for implementing and formally reasoning about smart contracts on the blockchain. IELE was designed by specifying its semantics formally in the K framework. Its implementation, a IELE virtual machine (VM), as well as a formal verification tool for IELE smart contracts, were automatically generated from the formal specification. The automatically generated formal verification tool allows us to formally verify smart contracts without any gap between the verifier and the actual VM. A compiler from Solidity, the predominant high- level language for smart contracts, to IELE has also been (manually) implemented, so Ethereum contracts can now also be executed on IELE.
PDF, BIB

Personal tools
Namespaces

Variants
Actions
Navigation