李希萌
博士，副教授，硕士生导师（北二区教学楼217室，lixm@cnu.edu.cn）
个人简介
2016年初于丹麦技术大学（Technical University of Denmark）获博士学位。2015至2016年在丹麦技术大学开展博士后研究，2016年至2018年于德国达姆施塔特工业大学（TU Darmstadt）开展博士后研究，2018年起在yl9193永利工作。在COLA、JSA、ESORICS、APLAS、ICFEM等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, 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]
李希萌, 王国辉, 张倩颖, 施智平*, 关永. 基于函数式语义的循环和递归程序结构通用证明技术. 软件学报, 在线发表(2022.03.24).
韩宁,李希萌*,张倩颖,王国辉,施智平,关永:以太坊中间语言的可执行语义.软件学报, 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]
学术报告
智能合约的演绎验证（中科院软件所，2021.6）
消息传递系统中信息流安全的组合式验证（北京大学，2018.11）
主要课程
算法设计与分析、数据结构、编译器设计实践等
主要荣誉
2021年度永利官网青年标兵
2020、2022年度yl9193永利考核优秀人员
2018年度永利官网军训工作先进个人
CCF期刊Computer Languages, Systems and Structures杰出贡献审稿人（2018）