Smart contracts are programs that automatically execute on blockchains when some conditions are verified. They encode the legally relevant events needed to satisfy the terms of an agreement and are usually defined by using procedural languages, even if some recent proposals investigated the possibility of using logic formalisms. However, existing logic-based initiatives are rather limited since they only enable the formal checking of properties of a single smart contract, totally neglecting its possible interactions with other smart contracts running on the same blockchain. This paper proposes a framework, called SCRea, that works on a set of smart contracts specified as Linear Temporal Logic (LTL) formulas. SCRea enables to reason about smart contracts considered individually or by considering them as running cooperatively or competitively on the same blockchain.

Reasoning about Smart Contracts via LTL Encoding

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

Abstract

Smart contracts are programs that automatically execute on blockchains when some conditions are verified. They encode the legally relevant events needed to satisfy the terms of an agreement and are usually defined by using procedural languages, even if some recent proposals investigated the possibility of using logic formalisms. However, existing logic-based initiatives are rather limited since they only enable the formal checking of properties of a single smart contract, totally neglecting its possible interactions with other smart contracts running on the same blockchain. This paper proposes a framework, called SCRea, that works on a set of smart contracts specified as Linear Temporal Logic (LTL) formulas. SCRea enables to reason about smart contracts considered individually or by considering them as running cooperatively or competitively on the same blockchain.
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/339163
 Attenzione

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

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