李希萌
博士，副教授，硕士生导师（北二区教学楼217室，lixm@cnu.edu.cn）
个人简介
2016年初于丹麦技术大学（Technical University of Denmark）获博士学位。2015至2016年在丹麦技术大学开展博士后研究，2016年至2018年于德国达姆施塔特工业大学（TU Darmstadt）开展博士后研究，2018年起在新葡萄8883官网AMG工作。在ETAPS、ESORICS、JSA等CCF推荐会议、期刊发表论文20余篇。担任中国计算机学会（CCF）形式化方法专委会委员，Computer Languages, Systems and Structures、软件学报等CCF期刊审稿人。
研究方向
形式化方法、软件验证
科研项目
某航天操作系统消息队列模块的形式化验证，横向项目，2022-2023（主持）
国家自然科学基金青年项目，面向完整性和可用性的智能合约形式化分析与修复方法研究，62002246，2021—2023（主持）
北京市教委科技计划一般项目，超性质的类型系统及其在智能合约验证中的应用，KM202010028010，2020—2022（主持）
德国BMBF项目CRISP IP2 --- Secure, Component-based Development of Large Software Systems，2016—2018（参加）
欧盟Artemis项目SESAMO --- Security and Safety Modelling，2012—2015（参加）
学生指导
指导研究生开展工作的主要方向：
关键基础软件的形式化验证
区块链智能合约的形式化验证
并发、分布式软件正确性、安全性验证的可靠方法
研究意义：基础软件自主可控、安全可靠是国家面临的重要问题。航空航天、数字金融等领域所使用复杂软件系统的正确、安全运行关乎生命、财产安全。形式化验证为安全攸关系统提供最高级别的正确性、安全性保障。
学术论文
Ximeng Li, Shanyan Chen, Yong Guan, Qianying Zhang, Guohui Wang, Zhiping Shi*: Refinement Verification of OS Services based on a Verified Preemptive Microkernel. In Proceedings of International Conference on Fundamental Approaches to Software Engineering (FASE), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), pp. 188-209, 2024. [CCF]
Ximeng Li, Qianying Zhang, Guohui Wang, Zhiping Shi*, Yong Guan: A Unified Proof Technique for Verifying Program Correctness with Big-step Semantics. Journal of Systems Architecture (JSA), 136: 1-22, 2023. [CCF, SCI]
Ximeng Li*, Qianying Zhang, Guohui Wang, Zhiping Shi*, Yong Guan*: Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics. In Proceedings of Symposium on Dependable Software Engineering – Theories, Tools, and Applications (SETTA), 2021. [CCF]
Ning Han, Ximeng Li*, Guohui Wang, Zhiping Shi, Yong Guan: Formal Verification of Atomicity Requirements for Smart Contracts. In Proceedings of the 18th Asian Symposium on Programming Languages and Systems (APLAS), pp. 44-64, 2020. [CCF]
Xiangyu Chen, Ximeng Li*, Qianying Zhang, Zhiping Shi, Yong Guan: Formalizing the Transaction Flow Process of Hyperledger Fabric. In Proceedings of the 22st International Conference on Formal Engineering Methods (ICFEM) pp. 233-250, 2020. [CCF]
Ximeng Li*, Flemming Nielson, Hanne Riis Nielson: Enforcing globally dependent flow policies in message-passing systems. Journal of Computer Languages (COLA), Vol 54, pp. 1-46, 2019. [SCI]
Ximeng Li*, Zhiping Shi*, Qianying Zhang, Guohui Wang, Yong Guan, Ning Han: Towards Verifying Ethereum Smart Contracts at IntermediateLanguage Level. In Proceedings of the 21st International Conference on Formal Engineering Methods; (ICFEM), pp. 121-137, 2019. [CCF]
Ximeng Li, Xi Wu, Alberto Lluch Lafuente, Flemming Nielson, Hanne Riis Nielson: A Coordination Language for Databases. In Logical Methods in Computer Science (LMCS), Vol 13(1:10), pp. 1-51. 2017. [CCF, SCI]
Ximeng Li*, Heiko Mantel*, Markus Tasch*: Taming Message-Passing Communication in Compositional Reasoning about Confidentiality. In Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS), pp. 45-66. 2017. [CCF]
Ximeng Li*, Flemming Nielson, Hanne Riis Nielson, Xinyu Feng: Disjunctive Information Flow for Communicating Processes. In Proceedings of the 10th International Symposium on Trustworthy Global Computing (TGC), pp. 95-111. 2016. [EI]
Ximeng Li*, Flemming Nielson, Hanne Riis Nielson: Factorization of Behavioral Integrity. In Proceedings of the 20th European Symposium on Research in Computer Security (ESORICS), pp. 500-519. 2015. [CCF]
张林雁,李希萌*,施智平,关永,曹钦翔,张倩颖.微内核操作系统互斥量模块功能正确性的形式化验证.软件学报,2024,35(9):4179-4192.
李希萌,王国辉,张倩颖,施智平*,关永.基于函数式语义的循环和递归程序结构通用证明技术.软件学报,2023,34(8):3686-3707.
韩宁,李希萌*,张倩颖,王国辉,施智平,关永:以太坊中间语言的可执行语义.软件学报, 2021, 32(6):1717-1732.
专著（合著）
Zhiping Shi, Yong Guan, Ximeng Li: Formalization of Complex Analysis and Matrix Theory, Tsinghua University Press and Springer Nature Singapore Pte Ltd. 2020.
博士论文
Fine-grained Information Flow for Concurrent Computation, Technical University of Denmark, 2016. [https:// orbit.dtu.dk/en/publications/fine-grained-information-flow-for-concurrent-computation]
学术报告
抢占式OS内核扩展服务的精化验证与全局性质验证（定理证明理论与应用研讨会，上海交通大学，2024.9）
抢占式OS内核扩展服务的形式化验证（CCF秀湖会议第十八期，苏州，2024.8）
智能合约的演绎验证（中科院软件所，2021.6）
消息传递系统中信息流安全的组合式验证（北京大学，2018.11）
主要课程
算法设计与分析、数据结构、编译器设计实践等
主要荣誉
2021年度首都师范大学青年标兵
2020、2022年度新葡萄8883官网AMG考核优秀人员
2018年度首都师范大学军训工作先进个人
CCF期刊Computer Languages, Systems and Structures杰出贡献审稿人（2018）