Smart contracts are programs deployed on blockchains that automatically execute when some conditions are verified to satisfy the terms of an agreement. They are usually programmed in procedural languages even if some recent proposals use logic for their specification and verification. However, existing logic-based initiatives only enable the formal checking of properties of a single smart contract independently from the other smart contracts running on the same blockchain. This paper proposes a framework, called SCRea, that works on a set of smart contracts encoded in Linear Temporal Logics. SCRea can work offline or at runtime to verify whether the execution of each smart contract is compatible with the execution of the others and, in case, provides a particular order of execution ensuring that the preconditions of each smart contract are verified before its execution.

Reasoning About Smart Contracts Encoded in LTL

Fionda V.;Greco G.;Mastratisi M. A.
2022-01-01

Abstract

Smart contracts are programs deployed on blockchains that automatically execute when some conditions are verified to satisfy the terms of an agreement. They are usually programmed in procedural languages even if some recent proposals use logic for their specification and verification. However, existing logic-based initiatives only enable the formal checking of properties of a single smart contract independently from the other smart contracts running on the same blockchain. This paper proposes a framework, called SCRea, that works on a set of smart contracts encoded in Linear Temporal Logics. SCRea can work offline or at runtime to verify whether the execution of each smart contract is compatible with the execution of the others and, in case, provides a particular order of execution ensuring that the preconditions of each smart contract are verified before its execution.
978-3-031-08420-1
978-3-031-08421-8
Linear temporal logic
Reasoning
Smart contracts
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11770/336824
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact