Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Verification of Smart Con… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Verification of Smart Contract Business Logic: Exploiting a Java Source Code Verifier

Paper i proceeding
Författare Wolfgang Ahrendt
Richard Bubel
Joshua Ellul
Gordon J. Pace
Raúl Pardo
Vincent Rebiscoul
Gerardo Schneider
Publicerad i Lecture Notes in Computer Science: Eigth International Conference on Fundamentals of Software Engineering (FSEN'19), volume 11761 of LNCS, pages 228-243
ISSN 0302-9743
Förlag Springer
Publiceringsår 2019
Publicerad vid Institutionen för data- och informationsteknik (GU)
Språk en
Länkar dx.doi.org/10.1007/978-3-030-31517-...
Ämneskategorier Data- och informationsvetenskap, Datorteknik

Sammanfattning

© 2019, IFIP International Federation for Information Processing. 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.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?