基本信息

李勇坚 男 硕导 中国科学院软件研究所
电子邮件: 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) 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
学生毕业去向
曾奶举--(先转博,后去)招商银行总行
于宝新 -- 中国农业银行软件开发部
哈晓琳--小米公司
曹燊--小米公司
段凯强--微软工程院