...
Ref1: Formal Verification of Smart Contracts - http://delivery.acm.org/10.1145/3000000/2993611/p91-bhargavan.pdf?ip=79.103.143.114&id=2993611&acc=OA&key=4D4702B0C3E38B35%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35%2EB7370FA72C089961&__acm__=1560061804_eacbf9bf1eef5530d0b182afd9b0a89a
2. ZEUS verification for Hyperledger Fabric and Ethereum Smart Contracts
abstract—A smart contract is hard to patch for bugs once it is deployed, irrespective of the money it holds. A recent bug caused losses worth around $50 million of cryptocurrency. We present ZEUS—a framework to verify the correctness and validate the fairness of smart contracts. We consider correctness as adherence to safe programming practices, while fairness is adherence to agreed upon higher-level business logic. ZEUSleverages both abstract interpretation and symbolic model checking, along with the power of constrained horn clauses to quickly verify contracts for safety. We have built a prototype of ZEUSfor Ethereumand Fabric blockchain platforms and evaluated it with over22.4K smart contracts. Our evaluation indicates that about 94.6%of contracts (containing cryptocurrency worth more than $0.5billion) are vulnerable. ZEUSis sound with zero false negatives and has a low false-positive rate, with an order of magnitude improvement in analysis time as compared to prior art.
Ref1: ZEUS: Analyzing Safety of Smart Contracts - http://pages.cpsc.ucalgary.ca/~joel.reardon/blockchain/readings/ndss2018_09-1_Kalra_paper.pdf