基本信息
李勇坚男硕导中国科学院软件研究所
电子邮件： 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山东大学威海分校学士

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

学位 -- 工学博士学位


出版信息
发表论文（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


指导学生已指导学生
于宝新**
哈晓琳**
曹燊**
段凯强**
现指导学生
曹嘉伦 **

学生毕业去向

曾奶举--（先转博，后去)招商银行总行
于宝新-- 中国农业银行软件开发部
哈晓琳--小米公司
曹燊--小米公司
段凯强--微软工程院