IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Author(s)
Kasampalis, Theodoros
Guth, Dwight
Moore, Brandon
Serbanuta, Traian Florin
Zhang, Yi
Filaretti, Daniele
Serbanuta, Virgil
Johnson, Ralph
Roşu, Grigore
Issue Date
2019-07-16
Keyword(s)
programming language design
compiler
formal semantics
blockchain
smart contracts
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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
