ETD

• property based testing
• Solidity

Property-Based Testing (PBT) is a useful approach for verifying the correctness of programs. The Ethereum Virtual Machine (EVM), which is used to run smart contracts, introduces the concept of "gas" as a unit of execution cost that must be paid by whoever invokes the contract.
In the context of the EVM, execution costs become a concern for program correctness and must be tested accordingly. This thesis proposes a type system to enable PBT on Solidity smart contracts based on the TinySol language.