Advancements in invariants-based smart contract analysis and verification call for tools that reliably and efficiently check semantic difference between invariants.These invariants, logical expressions that should hold in blockchain transactions are enforced through require/assert statements in Solidity smart contracts.  We present SInDi, a semantic invariant differencing tool for Solidity contracts that symbolically checks the differences of any two given invariants and quickly generates a verdict. Our evaluation on real-world smart contracts demonstrates SInDi's accuracy of 100% and efficiency of 0.09 seconds on average per verdict compared to human verdicts. Furthermore, we develop an invariant denoising pipeline based on SInDi that effectively removes up to 41.8% of weak dynamically-mined invariants to facilitate further analysis and verification tasks based on these auto-generated invariants.

@techreport{Eshghie1956137,
 author = {Eshghie, Mojtaba and Andersson Kasche, Gustav and Artho, Cyrille and Monperrus, Martin},
 institution = {KTH, Theoretical Computer Science, TCS},
 title = {SInDi: Semantic Invariant Differencing For Solidity Smart Contracts},
}