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

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

[29] Nehai Z, Piriou PY, Daumas F. Model-Checking of smart contracts. In: Proc. of the 2018 IEEE Int’l Conf. on Internet of Things
and IEEE Green Computing and Communications and IEEE Cyber, Physical and Social Computing and IEEE Smart Data. IEEE,
2018. 980−987. [doi: 10.1109/Cybermatics_2018.2018.00185]
[30] Kalra S, Goel S, Dhawan M, Sharma S. ZEUS: Analyzing safety of smart contracts. In: Proc. of the Network and Distributed
System Security Symp.. The Internet Society, 2018. [doi: 10.14722/NDSS.2018.23082]
[31] Leinenbach D, Paul W, Petrova E. Towards the formal verification of a C0 compiler: Code generation and implementation
correctness. In: Aichernig BK, Beckert B, eds. Proc. of the IEEE Int’l Conf. on Software Engineering and Formal Methods. IEEE
Computer Society, 2005. 2−12. [doi: 10.1109/SEFM.2005.51]
[32] Blazy S, Leroy X. Mechanized semantics for the clight subset of the c language. Journal of Automated Reasoning, 2009,43(3):
263−288. [doi: 10.1007/s10817-009-9148-3]
[33] Ellison C, Roşu G. An executable formal semantics of C with applications. In: Field J, Hicks M, eds. Proc. of the 39th ACM
SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM, 2012. 533−544. [doi: 10.1145/2103656. 2103719]
[34] Wasserrab D, Nipkow T, Snelting G, Tip F. An operational semantics and type safety proof for multiple inheritance in C++. In:
Tarr PL, Cook WR, eds. Proc. of the 21th Annual ACM SIGPLAN Conf. on Object-Oriented Programming Systems, Languages,
and Applications. ACM, 2006. 345−362. [doi: 10.1145/1167473.1167503]
[35] Norrish M. A formal semantics for C++. Technical Report, Australia: NICTA, 2008. 1−124.
[36] Drossopoulou S, Eisenbach S. Towards an operational semantics and proof of type soundness for Java. In: Proc. of the Formal
Syntax and Semantics of Java. 1998. 1523.
[37] Bogdanaş D, Roşu G. K-Java: A complete semantics of Java. In: Rajamani SK, Walker D, eds. Proc. of the 42nd Annual ACM
SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM, 2015. 445−456. [doi: 10.1145/2676726. 2676982]
[38] Nipkow T, Wenzel M, Paulson LC. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, 2002. 1−223. [doi:
10.1007/ 3-540-45949-9]
[39] ERC-20 token standard. 2019. https://github.com/ethereum/EIPs/blob/master/EIPS/eip-20.md

附中文参考文献:
[5] 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33−61. http://www.jos.org.cn/1000-9825/5652.htm [doi:
10.13328/j.cnki.jos.005652]

韩宁(1996－),女,硕士生,主要研究领域为 王国辉(1984－),男,博士,实验师,CCF 专
智能合约,形式化验证. 业会员,主要研究领域为高可靠嵌入式系
统与定理证明.

李希萌(1987－),男,博士,讲师,CCF 专业 施智平(1974－),男,博士,教授,博士生导
会员,主要研究领域为形式化验证,区块链 师,CCF 高级会员,主要研究领域为形式化
系统可靠性,信息流安全. 方法,人工智能.

张倩颖(1986－),女,博士,讲师,CCF 专业 关永 (1966－ ), 男 ,博士 ,教授 , 博 士生导
会员,主要研究领域为嵌入式操作系统,系 师,CCF 专业会员,主要研究领域为形式化
统安全,形式化验证. 验证,高可靠嵌入式系统,机器人.