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

3586 软件学报 2025 年第 36 卷第 8 期

on Computer-aided Verification. New York: Springer, 2019. 515–533. [doi: 10.1007/978-3-030-25543-5_29]
[19] Zhang LP, Zhao YW, Li JX. A comprehensive specification and verification of the L4 microkernel API. In: Proc. of the 30th Int’l Conf.
on Tools and Algorithms for the Construction and Analysis of Systems. Luxembourg: ACM, 2024. 217–234. [doi: 10.1007/978-3-031-
57249-4_11]
[20] Nipkow T, Wenzel M, Paulson LC. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Berlin: Springer, 2002. [doi: 10.1007/3-540-
45949-9]
[21] Huet GP, Kahn G, Paulin-Mohring C. The Coq proof assistant: A tutorial. 1997. https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf
[22] Owre S, Rushby JM, Shankar N. PVS: A prototype verification system. In: Proc. of the 11th Int’l Conf. on Automated Deduction.
Saratoga Springs: Springer, 1992. 748–752. [doi: 10.1007/3-540-55602-8_217]
[23] Jasti NVK, Kodali R. Lean production: Literature review and trends. Int’l Journal of Production Research, 2015, 53(3): 867–885. [doi: 10.
1080/00207543.2014.937508]

附中文参考文献:
[9] 许峰唯. 抢占式操作系统内核验证框架的设计和实现 [博士学位论文]. 合肥: 中国科学技术大学, 2016.

徐家乐(2000－), 男, 硕士生, CCF 学生会员, 主 崔舍承(1999－), 男, 硕士, 主要研究领域为并发
要研究领域为形式化方法. 软件测试.

王淑灵(1981－), 女, 博士, 副研究员, CCF 专业 吴鹏(1977－), 男, 博士, 副研究员, CCF 高级会

会员, 主要研究领域为形式化方法, 混成系统, 软 员, 主要研究领域为形式化方法, 并发测试, 机器

件验证. 学习.

李黎明(1978－), 男, 博士, 助理研究员, 主要研 谭宇(1988－), 男, 博士, 工程师, 主要研究领域

究领域为形式化验证. 为形式化方法, 操作系统技术, 软件工程.

詹博华(1989－), 男, 博士, CCF 专业会员, 主要 张学军(1978－), 男, 研究员, 主要研究领域为嵌

研究领域为形式化方法, 定理证明, 程序验证. 入式软件, 软件工程.

吕毅(1972－), 男, 博士, 副研究员, CCF 专业会 詹乃军(1971－), 男, 博士, 教授, 博士生导师,

员, 主要研究领域为并发理论, 形式化方法. CCF 杰出会员, 主要研究领域为形式化方法, 信

息物理融合系统, 程序验证.

代艺博(1999－), 男, 硕士, 主要研究领域为形式

化验证, 并发理论.