形式化方法、形式验证、机器学习、网络安全

对以下方向感兴趣的高年级本科生，欢迎联系我（包括实习、硕士研究生保送推荐与考试）。
1、程序的形式化分析与验证（例如硬件程序、软件程序、算法的正确性），
2、机器学习与形式化分析的结合（比如关联分析、决策树、深度学习等），
3、网络安全的形式化分析（比如认证协议、匿名协议、第三方认证协议等），
4、定理证明的自动化（如证明的自动生成，归纳证明，归纳不变式的自动构造等）。

(考生需要准备基于数据结构+算法的上机实测）

更多信息请访问个人主页：http://lcs.ios.ac.cn/~lyj238

081202-计算机软件与理论
085211-计算机技术

网络与并发实时系统的设计与分析
带参协议验证
机器学习

1998-03--2001-07   上海交通大学   博士
1995-09--1998-03   上海大学   硕士
1991-09--1995-07   山东大学威海分校   学士

上海交通大学 --20010814 研究生毕业

-- 工学博士学位

   

[1] 李勇坚. Accelerated Verification of Parametric Protocols with Decision Trees. International Conference on Computer Design 2020. 2020, [2] Li, Yongjian, Cao, Jialun, Pang, Jun, IEEE. A Learning-based Framework for Automatic Parameterized Verification. 2019 IEEE 37TH INTERNATIONAL CONFERENCE ON COMPUTER DESIGN (ICCD 2019)null. 2019, 450-459, [3] 李勇坚. 基于学习的缓存一致性协议带参验证. 电子产品世界. 2019, 26(1): 82-83, http://lib.cqvip.com/Qikan/Article/Detail?id=7001128659.
[4] Li, Yongjian, Duan, Kaiqiang, Jansen, David N, Pang, Jun, Zhang, Lijun, Lv, Yi, Cai, Shaowei. An Automatic Proving Approach to Parameterized Verification. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC[J]. 2018, 19(4): https://www.webofscience.com/wos/woscc/full-record/WOS:000452804000004.
[5] Li, Yongjian, Cao, Jialun, Duan, Kaiqiang, IEEE. An Automatic Parameterized Verification of FLASH Cache Coherence Protocol. 2018 IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS 2018)null. 2018, 47-58, http://dx.doi.org/10.1109/QRS.2018.00018.
[6] 段凯强, 李勇坚. 基于带参系统Murphi模型的SMV自动建模. 计算机系统应用. 2016, 178-182, http://lib.cqvip.com/Qikan/Article/Detail?id=670591698.
[7] Li, Yongjian, Duan, Kaiqiang, Lv, Yi, Pang, Jun, Cai, Shaowei, IEEE. A Novel Approach to Parameterized Verification of Cache Coherence Protocols. PROCEEDINGS OF THE 34TH IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN (ICCD)null. 2016, 560-567, [8] 贾娟娟, 施智平, 关永, 李勇坚, 魏洪兴. ROS中XML-RPC协议实现的形式化验证. 小型微型计算机系统[J]. 2015, 36(12): 2629-2633, [9] 李勇坚. An Automatic Framework for Proving Parameterized Cache Coherence Protocols.. The 13th International Symposium on Automated Technology for Verification and Analysis (ATVA), Springer,. 2015, [10] Li, Yongjian, Pang, Jun. Formalizing provable anonymity in Isabelle/HOL. FORMAL ASPECTS OF COMPUTING[J]. 2015, 27(2): 255-282, https://www.webofscience.com/wos/woscc/full-record/WOS:000349854100003.
[11] 曹燊, 李勇坚. 基于不变量查找的German协议验证. 计算机系统应用. 2015, 24(11): 173-178, http://lib.cqvip.com/Qikan/Article/Detail?id=666512145.
[12] Li Yongjian, Pang Jun. A Strand Space Approach to Provable Anonymity. 2nd International Workshop of Formal Techniques for Safety-Critical Systems, FTSCS 2013null. 2014, 71-87, http://ir.iscas.ac.cn/handle/311060/16629.
[13] Li, Yongjian, Zeng, Naiju, Hung, William N N, Song, Xiaoyu. Combining Symmetry Reduction with Generalized Symbolic Trajectory Evaluation. COMPUTER JOURNAL[J]. 2014, 57(1): 115-128, https://www.webofscience.com/wos/woscc/full-record/WOS:000329132400008.
[14] 哈晓琳, 李勇坚. 改进的布尔公式学习算法. 计算机系统应用. 2014, 23(9): 83-88, http://lib.cqvip.com/Qikan/Article/Detail?id=662074788.
[15] Li, Yongjian, Pang, Jun. An inductive approach to strand spaces. FORMAL ASPECTS OF COMPUTING[J]. 2013, 25(4): 465-501, http://dx.doi.org/10.1007/s00165-011-0187-2.
[16] 李勇坚. An inductive approach to strand space theory. Formal Aspects of Computing. 2013, [17] Li, Yongjian, Song, Xiaoyu, Li, Xiaojuan, Shen, H, Sang, Y, Li, Y, Qian, D, Zomaya, AY. On the formal modeling of inductive verification for cryptographical protocols. 2012 13TH INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED COMPUTING, APPLICATIONS, AND TECHNOLOGIES (PDCAT 2012)null. 2012, 201-206, http://dx.doi.org/10.1109/PDCAT.2012.104.
[18] 李勇坚. Combining Theorem Proving and Symbolic Trajectory Evaluation in THM&STE. Haifa Verification conference (HVC) 2013. LNCS 7261, Springer.. 2012, [19] Li, Yongjian, Hung, William N N, Song, Xiaoyu, Zeng, Naiju. Exploring structural symmetry automatically in symbolic trajectory evaluation. FORMAL METHODS IN SYSTEM DESIGN[J]. 2011, 39(2): 117-143, https://www.webofscience.com/wos/woscc/full-record/WOS:000297597200002.
[20] Li Yongjian, Pang Jun. An inductive approach to provable anonymity. Proceedings of the 2011 6th International Conference on Availability, Reliability and Security, ARES 2011null. 2011, 454-459, http://ir.iscas.ac.cn/handle/311060/16229.
[21] Li Yongjian, Zeng Naiju, Hung William N N, Song Xiaoyu. Enhanced symbolic simulation of a round-robin arbiter. Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processorsnull. 2011, 102-107, http://ir.iscas.ac.cn/handle/311060/16253.
[22] Li, Yongjian, Hung, William N N, Song, Xiaoyu. A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL. THEORETICAL COMPUTER SCIENCE[J]. 2011, 412(25): 2746-2765, http://dx.doi.org/10.1016/j.tcs.2011.01.032.
[23] 李勇坚. Extending the Strand Space Method with Timestamps: Part I the Theory. Journal of information security. 2010, [24] Li, Yongjian, Xue, Rui. Design of a CIL connector to Spin. INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING[J]. 2008, 18(1): 65-91, https://www.webofscience.com/wos/woscc/full-record/WOS:000255159800004.
[25] Li Yongjian, ACM. Mechanized proofs for the Parameter Abstraction and Guard Strengthening Principle in Parameterized Verification of Cache Coherence Protocols. APPLIED COMPUTING 2007, VOL 1 AND 2null. 2007, 1534-1535, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000268215700293.
[26] Li Yongjian, Pang Jun, Munro DS, Shen H, Sheng QZ, Detmold H, Falkner KE, Izu C, Coddington PD, Alexander B, Zheng SQ. Extending the strand space method to verify Kerberos V. EIGHTH INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED COMPUTING, APPLICATIONS AND TECHNOLOGIES, PROCEEDINGSnull. 2007, 437-+, http://dx.doi.org/10.1109/.22.
[27] Li Yongjian, Pang Jun, IEEE Comp Soc. Generalized unsolicited tests for authentication protocol analysis. SEVENTH INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED COMPUTING, APPLICATIONS AND TECHNOLOGIES, PROCEEDINGSnull. 2006, 509-+, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000245099900097.
[28] Li Yongjian, Pang Jun, IEEE Comp Soc. Generalized unsolicited tests for authentication protocol analysis. SEVENTH INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED COMPUTING, APPLICATIONS AND TECHNOLOGIES, PROCEEDINGSnull. 2006, 509-+, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000245099900097.
[29] 李勇坚, 何积丰, 孙永强. Verilog代数语义研究. 软件学报. 2003, 14(3): 317-327, http://lib.cqvip.com/Qikan/Article/Detail?id=7473449.

   

（ 1 ） 基于归纳不变式的带参协议验证, 主持, 国家级, 2017-01--2019-12
（ 2 ） 一阶符号轨迹计算的模型检测, 主持, 国家级, 2012-01--2015-12
（ 3 ） 基于符号轨迹计值的形式化语义以及模型检测算法的研究, 主持, 国家级, 2007-01--2009-12
（ 4 ） 行车许可限速与RBC切换技术形式化验证, 主持, 院级, 2015-01--2015-12

已指导学生

于宝新  02  19581  

哈晓琳  02  19261  

曹燊  02  19261  

段凯强  02  19261  

现指导学生

曹嘉伦   02  19261  

曾奶举--（先转博，后去)招商银行总行

于宝新 -- 中国农业银行软件开发部 

哈晓琳--小米公司  

曹燊--小米公司   

段凯强--微软工程院