基本信息
李勇坚 男 硕导 中国科学院软件研究所
电子邮件: lyj238@ios.ac.cn
通信地址: 中关村南4街4号
邮政编码:
电子邮件: lyj238@ios.ac.cn
通信地址: 中关村南4街4号
邮政编码:
研究领域
形式化方法、形式验证、机器学习、网络安全
招生信息
对以下方向感兴趣的高年级本科生,欢迎联系我(包括实习、硕士研究生保送推荐与考试)。
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] Proceedings of the ACM on Programming LanguagesVolume 8Issue OOPSLA1Article No.: 141pp 1324–1350. 2024, 第 1 作者[2] 李勇坚. CHISELFV: A FORMAL VERIFICATION FRAMEWORK FOR CHISEL. Design, Automation and Test in Europe Conference. 2023, 第 1 作者 通讯作者 [3] 李勇坚. Accelerated Verification of Parametric Protocols with Decision Trees. International Conference on Computer Design 2020. 2020, 第 1 作者[4] 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). 2019, 第 1 作者450-459, [5] 李勇坚. 基于学习的缓存一致性协议带参验证. 电子产品世界[J]. 2019, 第 1 作者26(1): 82-83, http://lib.cqvip.com/Qikan/Article/Detail?id=7001128659.[6] 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, 第 1 作者 通讯作者 19(4): https://www.webofscience.com/wos/woscc/full-record/WOS:000452804000004.[7] 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). 2018, 第 1 作者47-58, http://dx.doi.org/10.1109/QRS.2018.00018.[8] 段凯强, 李勇坚. 基于带参系统Murphi模型的SMV自动建模. 计算机系统应用[J]. 2016, 第 2 作者178-182, http://lib.cqvip.com/Qikan/Article/Detail?id=670591698.[9] 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). 2016, 第 1 作者560-567, [10] Li, Yongjian, Pang, Jun. Formalizing provable anonymity in Isabelle/HOL. FORMAL ASPECTS OF COMPUTING[J]. 2015, 第 1 作者 通讯作者 27(2): 255-282, https://www.webofscience.com/wos/woscc/full-record/WOS:000349854100003.[11] 曹燊, 李勇坚. 基于不变量查找的German协议验证. 计算机系统应用[J]. 2015, 第 2 作者24(11): 173-178, http://lib.cqvip.com/Qikan/Article/Detail?id=666512145.[12] 贾娟娟, 施智平, 关永, 李勇坚, 魏洪兴. ROS中XML-RPC协议实现的形式化验证. 小型微型计算机系统[J]. 2015, 第 4 作者36(12): 2629-2633, http://xwxt.sict.ac.cn/CN/Y2015/V36/I12/2629.[13] 李勇坚. An Automatic Framework for Proving Parameterized Cache Coherence Protocols.. The 13th International Symposium on Automated Technology for Verification and Analysis (ATVA), Springer,. 2015, 第 1 作者[14] Li Yongjian, Pang Jun. A Strand Space Approach to Provable Anonymity. 2nd International Workshop of Formal Techniques for Safety-Critical Systems, FTSCS 2013. 2014, 第 1 作者71-87, http://ir.iscas.ac.cn/handle/311060/16629.[15] Li, Yongjian, Zeng, Naiju, Hung, William N N, Song, Xiaoyu. Combining Symmetry Reduction with Generalized Symbolic Trajectory Evaluation. COMPUTER JOURNAL[J]. 2014, 第 1 作者 通讯作者 57(1): 115-128, https://www.webofscience.com/wos/woscc/full-record/WOS:000329132400008.[16] 哈晓琳, 李勇坚. 改进的布尔公式学习算法. 计算机系统应用[J]. 2014, 第 2 作者23(9): 83-88, http://lib.cqvip.com/Qikan/Article/Detail?id=662074788.[17] Li, Yongjian, Pang, Jun. An inductive approach to strand spaces. FORMAL ASPECTS OF COMPUTING[J]. 2013, 第 1 作者 通讯作者 25(4): 465-501, http://dx.doi.org/10.1007/s00165-011-0187-2.[18] 李勇坚. An inductive approach to strand space theory. Formal Aspects of Computing. 2013, 第 1 作者[19] 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). 2012, 第 1 作者201-206, http://dx.doi.org/10.1109/PDCAT.2012.104.[20] 李勇坚. Combining Theorem Proving and Symbolic Trajectory Evaluation in THM&STE. Haifa Verification conference (HVC) 2013. LNCS 7261, Springer.. 2012, 第 1 作者[21] 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, 第 1 作者 通讯作者 39(2): 117-143, https://www.webofscience.com/wos/woscc/full-record/WOS:000297597200002.[22] Li Yongjian, Pang Jun. An inductive approach to provable anonymity. PROCEEDINGS OF THE 2011 6TH INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY AND SECURITY, ARES 2011. 2011, 第 1 作者454-459, http://ir.iscas.ac.cn/handle/311060/16229.[23] 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 PROCESSORS. 2011, 第 1 作者102-107, http://ir.iscas.ac.cn/handle/311060/16253.[24] Li, Yongjian, Hung, William N N, Song, Xiaoyu. A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL. THEORETICAL COMPUTER SCIENCE[J]. 2011, 第 1 作者 通讯作者 412(25): 2746-2765, http://dx.doi.org/10.1016/j.tcs.2011.01.032.[25] 李勇坚. Extending the Strand Space Method with Timestamps: Part I the Theory. Journal of information security. 2010, 第 1 作者[26] Li, Yongjian, Xue, Rui. Design of a CIL connector to Spin. INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING[J]. 2008, 第 1 作者 通讯作者 18(1): 65-91, https://www.webofscience.com/wos/woscc/full-record/WOS:000255159800004.[27] 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 2. 2007, 第 1 作者 通讯作者 1534-1535, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000268215700293.[28] 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, PROCEEDINGS. 2007, 第 1 作者437-+, http://dx.doi.org/10.1109/.22.[29] 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, PROCEEDINGS. 2006, 第 1 作者509-+, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000245099900097.[30] 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, PROCEEDINGS. 2006, 第 1 作者509-+, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000245099900097.[31] 李勇坚, 何积丰, 孙永强. Verilog代数语义研究. 软件学报[J]. 2003, 第 1 作者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
学生毕业去向
曾奶举--(先转博,后去)招商银行总行
于宝新 -- 中国农业银行软件开发部
哈晓琳--小米公司
曹燊--小米公司
段凯强--微软工程院