Sökning: id:"swepub:oai:research.chalmers.se:984cdcb9-db4a-45aa-bf1e-533bf854af57" >
Verification of Sma...
Verification of Smart Contract Business Logic: Exploiting a Java Source Code Verifier
-
- Ahrendt, Wolfgang, 1967 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Bubel, Richard, 1976 (författare)
- Technische Universität Darmstadt
-
- Ellul, Joshua (författare)
- University of Malta
-
visa fler...
-
- Pace, Gordon (författare)
- University of Malta
-
- Pardo Jimenez, Raul, 1988 (författare)
- Institut National de Recherche en Informatique et en Automatique (INRIA)
-
- Rebiscoul, Vincent (författare)
- École Normale Supérieure de Lyon
-
- Schneider, Gerardo, 1967 (författare)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik (GU),Department of Computer Science and Engineering (GU)
-
visa färre...
-
(creator_code:org_t)
- 2019-09-22
- 2019
- Engelska.
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 11761 LNCS, s. 228-243
- Relaterad länk:
-
https://research.cha...
-
visa fler...
-
https://doi.org/10.1...
-
https://gup.ub.gu.se...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datorteknik (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Engineering (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas