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.
2021-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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
