A Systematic Literature Review on Smart Contract Vulnerability Detection by Symbolic Execution

Symbolic execution emerges as a potent method for software testing, progressively tackling the unique complexities associated with smart contract testing. Leveraging path exploration and constraint-solving mechanisms, symbolic execution uncovers potential vulnerabilities in smart contracts, ones that other testing methodologies might overlook. An expanding suite of tools and frameworks, including Oyente, Mythril, and Osiris, facilitate the symbolic execution of smart contracts. This paper delves into the theoretical underpinnings of smart contracts and symbolic execution. Subsequently, we provide a comprehensive review of the prevailing smart contract vulnerability detection tools reliant on symbolic execution, assessing their performance and testing scope, among other aspects. Lastly, we deliberate on the prospective challenges and the trajectory of this field in the future.