李希萌
电子邮件:lixm@cnu.edu.cn 办公地点:北二区教学楼217室
研究方向:形式化方法(Formal Methods)——侧重软件程序正确性和安全性的验证方法、分布式数字账本架构和程序的验证。
教育背景:2016年初于丹麦技术大学(Technical University of Denmark)获博士学位。
工作经历:2015至2016年在丹麦技术大学开展博后研究,2016年至2018年于德国达姆施塔特工业大学(TU Darmstadt)开展博后研究。2018年起在首都师范大学工作,任讲师、硕士生导师,中国计算机学会(CCF)形式化方法专业委员会委员。
科研项目:
国家自然科学基金青年项目,面向完整性和可用性的智能合约形式化分析与修复方法研究,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: Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics. Accepted at Symposium on Dependable Software Engineering – Theories, Tools, and Applications (SETTA), 2021.
韩宁,李希萌*,张倩颖,王国辉,施智平,关永:以太坊中间语言的可执行语义.软件学报, 2021, 32(6):1717-1732. [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]
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]
Ximeng Li, Flemming Nielson, Hanne Riis Nielson: Enforcing globally dependent flow policies in message-passing systems. Journal of Computer Languages (Vol 54), 2019. [SCI]
Ximeng Li, Zhiping Shi, Qianying Zhang, Guohui Wang, Yong Guan, Ning Han: Towards Verifying Ethereum Smart Contracts at Intermediate Language 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.
Ximeng Li, Flemming Nielson, Hanne Riis Nielson: Future-dependent Flow Policies with Prophetic Variables. In Proceedings of the 11th Workshop on Programming Languages and Analysis for Security (PLAS), pp. 29-42. 2016.
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]
博士论文:
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)
ESORICS、APLAS、ICFEM、Coordination、TGC、PLAS等国际会议口头学术报告
专著(合著):
Zhiping Shi, Yong Guan, Ximeng Li: Formalization of Complex Analysis and Matrix Theory, Springer 2020.
主要课程:
算法设计与分析、数据结构、编译器设计实践等
学生培养:
航空航天、智能制造、数字金融等领域所使用复杂IT系统的正确、安全运行可关乎到人的生命、财产安全。形式化验证为安全攸关系统提供最高级别的正确性、安全性保障。
学生培养方向主要包括但不限于:
软件程序的正确性、安全性验证方法
分布式账本(如区块链)、智能合约的验证
欢迎对我的研究方向感兴趣的本科生、研究生进一步了解相关情况。