Predicate abstractions for smart contract validation

Smart contracts are immutable programs deployed on the blockchain that can manage significant assets. Because of this, verification and validation of smart contracts is of vital importance. Indeed, it is industrial practice to hire independent specialized companies to audit smart contracts before deployment. Auditors typically rely on a combination of tools and experience but still fail to identify problems in smart contracts before deployment, causing significant losses. In this paper, we propose using predicate abstraction to con- struct models which can be used by auditors to explore and validate smart contact behaviour at the function call level by proposing predicates that expose different aspects of the contract. We pro- pose predicates based on requires clauses and enum-type state variables as a starting point for contract validation and report on an evaluation on two different benchmarks