English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

A bug or error is a common problem that any software or computer program mayencounter. It can occur from badly writing the program, a typing error or badmemory management. However, errors can become a significant issue if the unsafeprogram is used for critical systems. Therefore, formal methods for these kindsof systems are greatly required. In this paper, we use a formal language thatperforms deductive verification on an Ethereum Blockchain application based onsmart contracts, which are self-executing digital contracts. Blockchain systemsmanipulate cryptocurrency and transaction information. Therefore , if a bugoccurs in the blockchain, serious consequences such as a loss of money canhappen. Thus, the aim of this paper is to propose a language dedicated todeductive verification, called Why3, as a new language for writing formal andverified smart contracts, thereby avoiding attacks exploiting such contractexecution vulnerabilities. We first write a Why3 smart contracts program; nextwe formulate specifications to be proved as absence of RunTime Error propertiesand functional properties, then we verify the behavior of the program using theWhy3 system. Finally we compile the Why3 contracts to the Ethereum VirtualMachine (EVM). Moreover, we give a set of generic mathematical statements thatallows verifying functional properties suited to any type of smart contractsholding cryptocurrency, showing that Why3 can be a suitable language to writesmart contracts. To illustrate our approach, we describe its application to arealistic industrial use case.

Deductive Proof of Ethereum Smart Contracts Using Why3