Page 123 - 《软件学报》2025年第9期

4034 软件学报 2025 年第 36 卷第 9 期

Hamilton: Springer, 2006. 460–475 [doi: 10.1007/11813040_31]
[25] Yang Z, Lei H. Lolisa: Formal syntax and semantics for a subset of the solidity programming language in mathematical tool Coq.
Mathematical Problems in Engineering, 2020, 2020: 6191537. [doi: 10.1155/2020/6191537]
[26] Yang Z, Lei H. FEther: An extensible definitional interpreter for smart-contract verifications in Coq. IEEE Access, 2019, 7:
37770–37791. [doi: 10.1109/ACCESS.2019.2905428]
[27] Jiao J, Kan SL, Lin SW, Sanan D, Liu Y, Sun J. Semantic understanding of smart contracts: Executable operational semantics of solidity.
In: Proc. of the 2020 IEEE Symp. on Security and Privacy. San Francisco: IEEE, 2020. 1695–1712. [doi: 10.1109/SP40000.2020.00066]
[28] Jiao J, Lin SW, Sun J. A generalized formal semantic framework for smart contracts. In: Proc. of the 23rd Int’l Conf. on Fundamental
Approaches to Software Engineering. Dublin: Springer, 2020. 75–96. [doi: 10.1007/978-3-030-45234-6_4]
[29] K semantic framework. 2024. https://kframework.org
[30] Marmsoler D, Brucker AD. A denotational semantics of Solidity in Isabelle/HOL. In: Proc. of the 19th Int’l Conf. on Software
Engineering and Formal Methods. Virtual Event: Springer, 2021. 403–422. [doi: 10.1007/978-3-030-92124-8_23]
[31] Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making smart contracts smarter. In: Proc. of the 2016 ACM SIGSAC Conf. on Computer
and Communications Security. Vienna: ACM, 2016. 254–269. [doi: 10.1145/2976749.2978309]
[32] Hildenbrandt E, Saxena M, Rodrigues N, Zhu XR, Daian P, Guth D, Moore B, Park D, Zhang Y, Stefanescu A, Rosu G. KEVM: A
complete formal semantics of the Ethereum virtual machine. In: Proc. of the 31st IEEE Computer Security Foundations Symp. (CSF
2018). Oxford: IEEE, 2018. 204–217. [doi: 10.1109/CSF.2018.00022]
[33] Stefănescu A, Park D, Yuwen SJ, Li YL, Roşu G. Semantics-based program verifiers for all languages. ACM SIGPLAN Notices, 2016,
51(10): 74–91. [doi: 10.1145/3022671.2984027]
[34] Grishchenko I, Maffei M, Schneidewind C. A semantic framework for the security analysis of Ethereum smart contracts. In: Proc. of the
7th Int’l Conf. on Principles of Security and Trust. Thessaloniki: Springer, 2018. 243–269. [doi: 10.1007/978-3-319-89722-6_10]
[35] Amani S, Bégel M, Bortin M, Staples M. Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. In: Proc. of the 7th ACM
SIGPLAN Int’l Conf. on Certified Programs and Proofs. Los Angeles: ACM, 2018. 66–77. [doi: 10.1145/3167084]

附中文参考文献:
[2] 张俊, 高文忠, 张应晨, 郑心湖, 杨柳青, 郝君, 戴潇潇. 运行于区块链上的智能分布式电力能源系统: 需求、概念、方法以及展望.
自动化学报, 2017, 43(9): 1544–1554. [doi: 10.16383/j.aas.2017.c160744]
[10] 钱鹏, 刘振广, 何钦铭, 黄步添, 田端正, 王勋. 智能合约安全漏洞检测技术研究综述. 软件学报, 2022, 33(8): 3059–3085. http://www.
jos.org.cn/1000-9825/6375.htm [doi: 10.13328/j.cnki.jos.006375]
[11] 王璞巍, 杨航天, 孟佶, 陈晋川, 杜小勇. 面向合同的智能合约的形式化定义及参考实现. 软件学报, 2019, 30(9): 2608–2619. http://
www.jos.org.cn/1000-9825/5773.htm [doi: 10.13328/j.cnki.jos.005773]
[12] 王小兵, 杨潇钰, 舒新峰, 赵亮. 面向 MSVL 的智能合约形式化验证. 软件学报, 2021, 32(6): 1849–1866. http://www.jos.org.cn/1000-
9825/6253.htm [doi: 10.13328/j.cnki.jos.006253]
[13] 朱云凯. 基于 MSVL 的智能合约建模与验证 [硕士学位论文]. 西安: 西安电子科技大学, 2020. [doi: 10.27389/d.cnki.gxadu.2020.
002974]
[18] 王猛. 基于动态执行的程序时序性质验证 [博士学位论文]. 西安: 西安电子科技大学, 2019. [doi: 10.27389/d.cnki.gxadu.2019.
000059]