Most of the existing smart contract symbolic execution tools perform analysis on bytecode, which loses high-level semantic information presented in source code. This makes interactive analysis tasks—such as visualization and debugging—extremely challenging, and significantly limits the tool usability.
With Shang-Wei Lin, Palina Tolmach, and Ye Liu, we present SolSEE, a source-level symbolic execution engine for Solidity smart contracts. We describe the design of SolSEE, highlight its key features, and demonstrate its usages through a Web-based user interface. SolSEE demonstrates advantages over other existing source-level analysis tools in the advanced Solidity language features it supports and analysis flexibility.
A paper [1] describing SolSEE is accepted at the FSE’22 Demonstration track. You can find the video demonstration of the tool below.
SolSEE Demo Video
References
- Lin, S.-W., Tolmach, P., Liu, Y., & Li, Y. (2022). SolSEE: A Source-Level Symbolic Execution Engine for Solidity. Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (FSE), 1687–1691.