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

对以下方向感兴趣的高年级本科生，欢迎联系我（包括实习、硕士研究生保送推荐与考试）。
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  

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

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

哈晓琳--小米公司  

曹燊--小米公司   

段凯强--微软工程院