Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction

Ye Liu, Yixuan Liu, Yi Li, and Cyrille Artho

In Proceedings of the 32nd IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER), 2025

Abstract: Smart contracts are computer programs running on blockchains to implement Decentralized Applications. The absence of contract specifications hinders routine tasks, such as contract understanding and testing. In this work, we propose a specification mining approach to infer contract specifications from past transaction histories. Our approach derives high-level behavioral automata of function invocations, accompanied by program invariants statistically inferred from the transaction histories. We implemented our approach as tool SMCON and evaluated it on eleven well-studied Azure benchmark smart contracts and six popular real-world DApp smart contracts. The experiments show that SMCON mines reasonably accurate specifications that can be used to enhance symbolic analysis of smart contracts achieving higher code coverage and up to 54% speedup, and facilitate DApp developers in maintaining high-quality documentation and test suites.

Cite:

@inproceedings{Liu2024SMS,
  author = {Liu, Ye and Liu, Yixuan and Li, Yi and Artho, Cyrille},
  booktitle = {Proceedings of the 32nd IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)},
  month = mar,
  title = {Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction},
  year = {2025}
}