IELE: A rigorously designed language and tool ecosystem for the blockchain

Theodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Florin Șerbănuță, Yi Zhang, Daniele Filaretti, Virgil Șerbănuță, Ralph Johnson, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationFormal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings
EditorsMaurice H. ter Beek, Annabelle McIver, José N. Oliveira
PublisherSpringer
Pages593-610
Number of pages18
ISBN (Print)9783030309411
DOIs
StatePublished - 2019
Event23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019 - Porto, Portugal
Duration: Oct 7 2019Oct 11 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11800 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019
CountryPortugal
CityPorto
Period10/7/1910/11/19

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'IELE: A rigorously designed language and tool ecosystem for the blockchain'. Together they form a unique fingerprint.

Cite this