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

王小兵 等: Solidity 到 MSVL 转换的等价性研究 4033

[2] Zhang J, Gao WZ, Zhang YC, Zheng XH, Yang LQ, Hao J, Dai XX. Blockchain based intelligent distributed electrical energy systems:
Needs, concepts, approaches and vision. Acta Automatica Sinica, 2017, 43(9): 1544–1554 (in Chinese with English abstract). [doi: 10.
16383/j.aas.2017.c160744]
[3] Buterin V. A next-generation smart contract and decentralized application platform. 2014. https://ethereum.org/en/whitepaper/
[4] Underwood S. Blockchain beyond bitcoin. Communications of the ACM, 2016, 59(11): 15–17. [doi: 10.1145/2994581]
[5] Delmolino K, Arnett M, Kosba A, Miller A, Shi E. Step by step towards creating a safe smart contract: Lessons and insights from a
cryptocurrency lab. In: Proc. of the 2016 Int’l Workshops on Financial Cryptography and Data Security. Christ Church: Springer, 2016.
79–94. [doi: 10.1007/978-3-662-53357-4_6]
[6] Szabo N. Formalizing and securing relationships on public networks. First Monday, 1997, 2(9). [doi: 10.5210/fm.v2i9.548]
[7] Clack CD, Bakshi VA, Braine L. Smart contract templates: Foundations, design landscape and research directions. arXiv:1608.00771v3,
2017.
[8] Mehar MI, Shier CL, Giambattista A, Gong E, Fletcher G, Sanayhie R, Kim HM, Laskowski M. Understanding a revolutionary and
flawed grand experiment in blockchain: The DAO attack. Journal of Cases on Information Technology (JCIT), 2019, 21(1): 19–32. [doi:
10.4018/JCIT.2019010102]
[9] Atzei N, Bartoletti M, Cimoli T. A survey of attacks on Ethereum smart contracts (SoK). In: Proc. of the 6th Int’l Conf. on Principles of
Security and Trust. Uppsala: Springer, 2017. 164–186. [doi: 10.1007/978-3-662-54455-6_8]
[10] Qian P, Liu ZG, He QM, Huang BT, Tian DZ, Wang X. Smart contract vulnerability detection technique: A survey. Ruan Jian Xue
Bao/Journal of Software, 2022, 33(8): 3059–3085 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6375.htm [doi: 10.
13328/j.cnki.jos.006375]
[11] Wang PW, Yang HT, Meng J, Chen JC, Du XY. Formal definition for classical smart contracts and reference implementation. Ruan Jian
Xue Bao/Journal of Software, 2019, 30(9): 2608–2619 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5773.htm
[doi: 10.13328/j.cnki.jos.005773]
[12] Wang XB, Yang XY, Shu XF, Zhao L. Formal verification of smart contract based on MSVL. Ruan Jian Xue Bao/Journal of Software,
2021, 32(6): 1849–1866 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6253.htm [doi: 10.13328/j.cnki.jos.006253]
[13] Zhu YK. A method based on MSVL for modeling and verifying the smart contract [MS. Thesis]. Xi’an: Xidian University, 2020 (in
Chinese with English abstract). [doi: 10.27389/d.cnki.gxadu.2020.002974]
[14] Wang M, Tian C, Zhang N, Duan ZH. Verifying full regular temporal properties of programs via dynamic program execution. IEEE
Trans. on Reliability, 2019, 68(3): 1101–1116. [doi: 10.1109/TR.2018.2876333]
[15] Ma YT, Duan ZH, Wang XB, Yang XX. An interpreter for framed tempura and its application. In: Proc. of the 1st Joint IEEE/IFIP Symp.
on Theoretical Aspects of Software Engineering. Shanghai: IEEE, 2007. 251–260. [doi: 10.1109/TASE.2007.10]
[16] Wang XB, Tian C, Duan ZH, Zhao L. MSVL: A typed language for temporal logic programming. Frontiers of Computer Science, 2017,
11(5): 762–785. [doi: 10.1007/s11704-016-6059-4]
[17] Zhang N, Duan ZH, Tian C. A mechanism of function calls in MSVL. Theoretical Computer Science, 2016, 654: 11–25. [doi: 10.1016/j.
tcs.2016.02.037]
[18] Wang M. Verifying full regular temporal properties of programs via dynamic program execution [Ph.D. Thesis]. Xi’an: Xidian
University, 2019 (in Chinese with English abstract). [doi: 10.27389/d.cnki.gxadu.2019.000059]
[19] Wang XB, Duan ZH, Zhao L. Formalizing and implementing types in MSVL. In: Proc. of the 3rd Int’l Workshop on Structured Object-
oriented Formal Language and Method. Queenstown: Springer, 2013. 62–75. [doi: 10.1007/978-3-319-04915-1_5]
[20] Zakrzewski J. Towards verification of Ethereum smart contracts: A formalization of core of Solidity. In: Proc. of the 10th Int’l Conf. on
Verified Software: Theories, Tools, and Experiments. Oxford: Springer, 2018. 229–247. [doi: 10.1007/978-3-030-03592-1_13]
[21] Velasco PP. Providing formal semantics for solidity to allow its verification [BS. Thesis]. Madrid: Universidad Complutense de Madrid,
2020.
[22] Dagnino F. A meta-theory for big-step semantics. ACM Trans. on Computational Logic, 2022, 23(3): 20. [doi: 10.1145/3522729]
[23] Kahn G. Natural semantics. In: Proc. of the 4th Annual Symp. on Theoretical Aspects of Computer Science. Passau: Springer, 1987.
22–39. [doi: 10.1007/BFb0039592]
[24] Blazy S, Dargaye Z, Leroy X. Formal verification of a C compiler front-end. In: Proc. of the 14th Int’l Symp. on Formal Methods.