TY - GEN
T1 - IELE
T2 - 23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019
AU - Kasampalis, Theodoros
AU - Guth, Dwight
AU - Moore, Brandon
AU - Șerbănuță, Traian Florin
AU - Zhang, Yi
AU - Filaretti, Daniele
AU - Șerbănuță, Virgil
AU - Johnson, Ralph
AU - Roşu, Grigore
N1 - Funding Information:
We are grateful to IOHK (http://iohk.io) for funding the IELE project, as well as for insightful discussions, encouragements and constructive criticisms along the way. The work on the K framework and its tooling was supported in part by NSF grant CNS 16-19275 and by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092.
Funding Information:
Acknowledgements. We are grateful to IOHK (http://iohk.io) for funding the IELE project, as well as for insightful discussions, encouragements and constructive criticisms along the way. The work on the K framework and its tooling was supported in part by NSF grant CNS 16-19275 and by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092.
Publisher Copyright:
© Springer Nature Switzerland AG 2019.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85076119712&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85076119712&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-30942-8_35
DO - 10.1007/978-3-030-30942-8_35
M3 - Conference contribution
AN - SCOPUS:85076119712
SN - 9783030309411
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 593
EP - 610
BT - Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings
A2 - ter Beek, Maurice H.
A2 - McIver, Annabelle
A2 - Oliveira, José N.
PB - Springer
Y2 - 7 October 2019 through 11 October 2019
ER -