Page 292 - 《软件学报》2021年第6期

1866 Journal of Software 软件学报 Vol.32, No.6, June 2021

[11] Zhao L, Wang X, Shu XF, Zhang N. A sound and complete proof system for a unified temporal logic. Theoretical Computer
Science, 2020,838:25−44.
[12] Duan ZH, Tian C. A unified model checking approach with projection temporal logic. In: Liu SY, Maibaum T, Araki K, eds. Proc.
of the ICFEM 2008. LNCS 5256. London: Springer-Verlag, 2008. 167−186. [doi: 10.1007/978-3-540-88194-0_12]
[13] Yang K, Duan ZH, Tian C, Zhang N. A compiler for MSVL and its applications. Theoretical Computer Science, 2018,749:2−16.
[14] Bhargavan K, Delignat-Lavaud A, Fournet C, Gollamudi A, Gonthier G, Kobeissi N, Kulatova N, Rastogi A, Sibut-Pinote T,
Swamy N, Zanella-Béguelin S. Formal verification of smart contracts: Short paper. In: Proc. of the PLAS 2016. 2016. 91−96. [doi:
10.1145/2993600.2993611]
[15] Fang Y. Research and implementation of formal verification technology based on Ethereum smart contract. University of Electronic
Science and Technology of China, 2019 (in Chinese with English abstract).
[16] Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making smart contracts smarter. In: Proc. of the CCS 2016. ACM, 2016. 254−269.
[17] Kalra S, Goel S, Dhawan M, Sharma S. ZEUS: Analyzing safety of smart contracts. In: Proc. of the NDSS 2018. 2018. 1−12.
[18] Hu K, Bai XM, Gao LC, Dong AQ. Formal verification method of smart contract. Journal of Information Security Research, 2016,
2(12):1080−1089 (in Chinese with English abstract). [doi: 10.3969/j.issn.2096-1057.2016.12.003]
[19] Hildenbrandt E, Saxena M, Rodrigues N, Zhu X, 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 IEEE 31st Computer Security Foundations Symp.
(CSF 2018). Oxford, 2018. 204−217.
[20] Clarke E, Grumberg O, Jha S, Lu Y, Veith H. Progress on the state explosion problem in model checking. In: Proc. of the
Informatics 2001. Berlin, Heidelberg: Springer-Verlag, 2001. 176−194.

附中文参考文献:
[15] 方言.基于以太坊智能合约的形式化验证技术研究与实现.电子科技大学,2019.
[18] 胡凯,白晓敏,高灵超,董爱强.智能合约的形式化验证方法.信息安全研究,2016,2(12):1080−1089. [doi: 10.3969/j.issn.2096-1057.
2016.12.003]

王小兵(1979－),男,博士,副教授,博士生 舒新峰(1975－),男,博士,教授,CCF 专业
导师,CCF 高级会员,主要研究领域为形式 会员,主要研究领域为可信软件技术及应
化方法,形式化验证,时序逻辑. 用,智能信息处理.

杨潇钰(1999－),女,硕士,CCF 学生会员, 赵亮(1984－),男,博士,副教授,CCF 专业
主要研究领域为形式化方法,形式化验证, 会员,主要研究领域为形式化方法,形式化
时序逻辑. 验证,时序逻辑.