%0 Conference Proceedings
%T Verification of Smart Contract Business Logic
%+ Chalmers University of Technology [Göteborg]
%+ Technische Universität Darmstadt - Technical University of Darmstadt (TU Darmstadt)
%+ University of Malta [Malta]
%+ Privacy Models, Architectures and Tools for the Information Society (PRIVATICS)
%+ École normale supérieure de Lyon (ENS de Lyon)
%+ Göteborgs Universitet = University of Gothenburg (GU)
%A Ahrendt, Wolfgang
%A Bubel, Richard
%A Ellul, Joshua
%A Pace, Gordon, J.
%A Pardo, Raúl
%A Rebiscoul, Vincent
%A Schneider, Gerardo
%Z Part 6: Program Analysis
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 8th International Conference on Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Hossein Hojjat
%Y Mieke Massink
%I Springer International Publishing
%3 Fundamentals of Software Engineering
%V LNCS-11761
%P 228-243
%8 2019-05-01
%D 2019
%R 10.1007/978-3-030-31517-7_16
%Z Computer Science [cs]Conference papers
%X Smart contracts have been argued to be a means of building trust between parties by providing a self-executing equivalent of legal contracts. And yet, code does not always perform what it was originally intended to do, which resulted in losses of millions of dollars. Static verification of smart contracts is thus a pressing need. This paper presents an approach to verifying smart contracts written in Solidity by automatically translating Solidity into Java and using KeY, a deductive Java verification tool. In particular, we solve the problem of rolling back the effects of aborted transactions by exploiting KeY’s native support of JavaCard transactions. We apply our approach to a smart contract which automates a casino system, and discuss how the approach addresses a number of known shortcomings of smart contract development in Solidity.
%G English
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-03769118/document
%2 https://inria.hal.science/hal-03769118/file/490001_1_En_16_Chapter.pdf
%L hal-03769118
%U https://inria.hal.science/hal-03769118
%~ ENS-LYON
%~ INRIA
%~ INSA-LYON
%~ INRIA-RHA
%~ INRIA_TEST
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-FSEN
%~ INRIA-RENGRE
%~ CITI
%~ INSA-GROUPE
%~ UDL
%~ UNIV-LYON
%~ INRIA-LYS
%~ IFIP-LNCS-11761
%~ INRIA-ALLEMAGNE