We provide three detailed case studies of vulnerabilities in smart contracts, and show how property-based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave's BAT token. The last example is, in fact, new, and was missed in the auditing process. We have implemented this testing in ConCert, a general executable model/specification of smart contract execution in the Coq proof assistant. ConCert contracts can be used to generate verified smart contracts in Tezos' LIGO and Concordium's rust language. We thus show the effectiveness of combining formal verification and property-based testing of smart contracts.

翻译：我们对智能合同中的弱点进行了三个详细的个案研究,并表明基于财产的测试如何发现这些弱点:1. Dexter1 象征性交换;2. iToken;3. Brave BAT 标志的ICO;3. 最后一个例子,事实上是新的,在审计过程中被遗漏了。我们在ConCert进行了这次测试,ConCert是Coq验证助理执行智能合同的一般可执行模式/具体情况。ConCert合同可用于在Tezos的LIGO和Concordium的生锈语言中生成经核实的智能合同。因此,我们展示了将正式核查与基于财产的智能合同测试相结合的有效性。