基本信息

李勇坚  男  硕导  中国科学院软件研究所 计算机科学国家重点实验室
电子邮件: lyj238@ios.ac.cn
通信地址: 中关村南4街4号
邮政编码: 100190

研究领域

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

招生信息

对以下方向感兴趣的高年级本科生,欢迎联系我(包括实习、硕士研究生保送推荐与考试)。
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) A Novel Approach to Parameterized Verification of Cache Coherence Protocols, IEEE 29th International Conference on Computer Design (ICCD),, 2016, 第 1 作者
(2) An Automatic Framework for Proving Parameterized Cache Coherence Protocols., The 13th International Symposium on Automated Technology for Verification and Analysis (ATVA), Springer,, 2015, 第 1 作者
(3) Formalizing provable anonymity in Isabelle/HOL. , formal aspects of computing, 2015, 第 1 作者
(4) Combining Symmetry Reduction with Generalized Symbolic Trajectory Evaluation, The computer journal, 2014, 第 1 作者
(5) An inductive approach to strand space theory, Formal Aspects of Computing, 2013, 第 1 作者
(6) Combining Theorem Proving and Symbolic Trajectory Evaluation in THM&STE, Haifa Verification conference (HVC) 2013. LNCS 7261, Springer., 2012, 第 1 作者
(7) Enhanced symbolic simulation of a round-robin arbiter., International conference on computer design, IEEE 29th International Conference on Computer Design, ICCD 2011, Amherst, MA, USA, IEEE Press., 2011, 第 1 作者
(8) A Novel Formalization of Symbolic Trajectory Evaluation Semantics in Isabelle/HOL, Theoretical Computer Science, 2011, 第 1 作者
(9) Exploring Structural Symmetry Automatically in Symbolic Trajectory Evaluation, Formal methods in system design, 2011, 第 1 作者
(10) Extending the Strand Space Method with Timestamps: Part I the Theory, Journal of information security, 2010, 第 1 作者
(11) Design of a CIL Connector to SPIN, The International Journal of Software Engineering and Knowledge Engineering, 2008, 第 1 作者
(12) Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols, ACM Symposium on Applied Computing (SAC 2007), 2007, 第 1 作者

科研活动

   
科研项目
( 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  

学生毕业去向

曾奶举--(先转博,后去)招商银行总行

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

哈晓琳--小米公司  

曹燊--小米公司   

段凯强--微软工程院