Page 88 - 《软件学报》2025年第8期

何韬 等: GhostFunc: 一种针对 Rust 操作系统内核的验证方法 3511

[20] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107–115. [doi: 10.1145/1538788.
1538814]
[21] Gonthier G. Formal proof—The four-color theorem. Notices of the AMS, 2008, 55(11): 1382–1393.
[22] David D, Micaela M. Diophantus’ 20th problem and fermat’s last theorem for n=4: Formalization of fermat’s proofs in the Coq proof
assistant. arXiv:cs/0510011, 2005.
[23] Jung R, Krebbers R, Jourdan JH, Bizjak A, Birkedal L, Dreyer D. Iris from the ground up: A modular foundation for higher-order
concurrent separation logic. Journal of Functional Programming, 2018, 28: e20. [doi: 10.1017/S0956796818000151]
[24] Jung R, Krebbers R, Birkedal L, Dreyer D. Higher-order ghost state. In: Proc. of the 21st ACM SIGPLAN Int’l Conf. on Functional
Programming (ICFP). Nara: Association for Computing Machinery, 2016. 256–269. [doi: 10.1145/2951913.2951943]
[25] Jung R, Swasey D, Sieczkowski F, Svendsen K, Turon A, Birkedal L, Dreyer D. Iris: Monoids and invariants as an orthogonal basis for
concurrent reasoning. ACM SIGPLAN Notices, 2015, 50(1): 637–650. [doi: 10.1145/2775051.2676980]

附中文参考文献:
[1] 王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报, 2019, 30(1): 33–61. http://www.jos.org.cn/1000-9825/5652.htm [doi:
10.13328/j.cnki.jos.005652]
[4] 乔磊, 杨孟飞, 谭彦亮, 蒲戈光, 杨桦. 基于 Event-B 的航天器内存管理系统形式化验证. 软件学报, 2017, 28(5): 1204–1220. http://
www.jos.org.cn/1000-9825/5218.htm [doi: 10.13328/j.cnki.jos.005218]

何韬(2000－), 男, 硕士生, 主要研究领域为操作 文艳军(1975－), 男, 博士, 教授, CCF 专业会员,
系统内核验证, Rust 程序验证. 主要研究领域为操作系统形式化验证, 可信软件
设计与验证.

董威(1976－), 男, 博士, 教授, 博士生导师, CCF
高级会员, 主要研究领域为软件分析与验证, 软
件度量与评估.