李勇坚 English

副教授
计算机科学国家重点实验室
中国科学院软件研究所

北京 8718 信箱 100190

电话. (86) (10) 62661645
邮箱:
  lyj238@ios.ac.cn

教育经历     研究方向     主要项目     主要论著    

 


教育经历

  • 博士:1998.3——2001.3 上海交通大学计算机科学与工程系 计算机软件与理论
  • 硕士:1995.9——1998.3 上海大学计算机科学与工程系 计算机软件与理论
  • 本科:1991.9——1995.7 山东大学威海分校计算机工程系

研究方向

  • 并发实时软件设计与分析方法
  • 计算机科学理论和软件理论
  • 机器学习
  • 大数据处理
  • 招生信息    

主要项目

  1. 全军共用信息系统装备预研项目“内生安全应用构造技术的子课题--应用软件构造工具集成与实例研究(2019-2021 ),110万, 主持.
  2. 国家自然科学基金:基于归纳不变式的带参协议验证61672503,2017.1 -2020.12),63万,项目负责人。
  3. 国家自然科学基金:基于一阶符号轨迹计算理论的模型检测(61170073,2011.1 -2015.12),56万,项目负责人。
  4.  国家自然科学基金:符号轨迹计算的形式化语义及模型检测算法研究(60603001,2007.1 -2009.12),18万,项目负责人。
  5. 模型检验技术在认证协议验证中的研究,中国科学院软件研究所基础研究课题基金,项目负责人。
  6. 基于串空间的协议分析方法的研究, 信息安全国家重点实验室开放课题,项目负责人。
  7. 高可信软件的形式化理论与方法—并发理论研究,参加者。
  8. 软件基础研究中的若干前沿问题, 参加者。

主要论著

    • Yongjian Li, Kaiqiang Duan, David N. Jansen, Jun Pang, Lijun Zhang, Yi Lv, and Shaowei Cai An Automatic Proving Approach to Parameterized Verification. ACM transaction on computation logic录用, 2018.

    • Yongjian Li, Jialun Cao, Jun Pang. L-CMP: An Automatic Learning-based Parameterized Verification Tool. IEEE/ACM International Conference on Automated Software Engineering (ASE-18) Tool-track, 2018.

    • Yongjian Li, Jialun Cao, Kaiqiang Duan. An Automatic Parameterized Verification of the FLASH Cache Coherence Protocol. The 18th IEEE conference on software quality and reliability and security(QRS-2018), 2018.

    • Yongjian Li, Kaiqiang Duan, Yi Lv, Jun Pang and Shaowei Cai. A Novel Approach to Parameterized Verification of Cache Coherence Protocols. IEEE 29th International Conference on Computer Design (ICCD), IEEE Press, 2016.

    • Yongjian Li, Jun Pang, Yi Lv, Dongrui Fan, Shen Cao and Kaiqiang Duan. paraVerifier: An Au- tomatic Framework for Proving Parameterized Cache Coherence Protocols. The 13th International Symposium on Automated Technology for Verification and Analysis (ATVA), Springer, 2015.

    • Yongjian Li, Jun Pang. Foramilzing provable anonymity in Isabelle/HOL. Formal Aspects of Computing, Springer, 2014.

    • Yongjian Li, Xiaoyu Song. On the formal modeling of inductive verification for cryptographical protocols. Accepted in The Thirteen International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT12), IEEE Computer Press, 2012.

    • Yongjian Li, Naiju Zeng, William N. N. Hung, Xiaoyu Song. Combining symmetry reduction with generalized symbolic trajectory evaluation. Accepted in The Computer Journal, Oxford Unversity Press, 2012.

    • Yongjian Li, Naiju Zeng, William N. N. Hung, Xiaoyu Song. Combining Theorem Proving and Symbolic Trajectory Evaluation in THM&STE. Haifa Verification conference (HVC) 2012, LNCS7261: 242-246

    • Yongjian Li, Jun Pang. An Inductive Approach to Provable Anonymity. Conference on Availability, Reliability and Security (ARES) 2011: 454-459, IEEE Press.

    • Yongjian Li, Naiju Zeng, William N. N. Hung, Xiaoyu Song. Enhanced symbolic simulation of a round-robin arbiter. International conference on computer design (ICCD) 2011:102-107, IEEE Press.

    • Yongjian Li, jun Pang. An inductive approach to strand space theory. Formal Aspects of Computing. Springer.

    • Yongjian li, William N. N. Hung, Xiaoyu Song. Automatically Exploring Structural Symmetry in Symbolic Trajectory Evaluation. Formal Methods in System Design 39(2): 117-143 (2011). Springer.

    • Yongjian li, William N. N. Hung, Xiaoyu Song. A Novel Formalization of Symbolic Trajectory Evaluation Semantics in Isabelle/HOL. Theoretical Computer Science: 2746-2765 (2011). Elsevier. 2011.01

    • Yongjian Li, Jun Pang. Extending the Strand Space Method with Timestamps: Part I the Theory. Jounal of Information Security, Vol.1. 45-55. doi: 10.4236/jis.2010.12007. October 2010.

    • Yongjian Li, Jun Pang. Extending the Strand Space Method with Timestamps: Part II Application to Kerberos V. Jounal of Information Security, Vol.1.56-67. doi:10.4236/jis.2010.12007. October 2010.

    • Li yongjian, Xue rui. Design of a CIL Connector to SPIN. International Journal of Software Engineering and Knowledge Engineering 18(1): 65-91. 2008.

    • Li yongjian, Xue rui. Using SPIN to Model Cryptographic Protocols. In proceedings of International Conference on Information Technology : 741-745, IEEE Press. April 2004.

    • Yongjian Li. The inductive approach to strand space theory. Proceedings of Formal Techniques for Networked and Distributed Systems-FORTE 2005, 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005, Lecture Notes in Computer Science 3731 : 547-552, Springer 2005. October 2005.

    • Yongjian Li, Jun Pang. Generalized Unsolicited Tests for Authentication Protocol Analysis. Proceedings of the International Conference on Parallel and Distributed Computing (PDCAT 2006): 509-514, IEEE CS Press. 2006.

    • Yongjian Li, Jun Pang. Extending the Strand Space Method to Verify Kerberos V. Proceedings of the International Conference on Parallel and Distributed Computing (PDCAT 2007): 437-444,IEEE CS Press. 2007.

    • Li yongjian, Liu XinXin. Towards a theory of bisimulation for the Higher-Order process calculi. Journal of computer science and technology, Vol 19(3): 352-363. 2004. 2004.

    • Yongjian Li. Contextual labelled semantics for Higher-Order process calculi. Electronic Notes in Theoretical Computer Science 138, 61-77, 2005. Elsevier. 2005.

    • Yongjian Li. Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols. 2007 ACM Symposium on Applied Computing (SAC 2007): 1534-1535, ACM Press. 2007.

    • Yongjian Li, Jifeng He, Yongqiang Sun. Verilog 代数语义研究. 软件学报,Vol.14. No.3. 2003.

    • Yongjian Li, Jifeng He, Yongqiang Sun. Verilog 操作语义研究. 软件学报,Vol.13 No.10, 2002.

    • Yongjian Li, Jifeng He, Yongqiang Sun. Verilog 形式化语义研究. 软件学报,Vol.12. No.10, 2001.

    • Yongjian Li, Jifeng He. Towards a theory of bisimulation for a fragment of Verilog. proceedings of 17th international parallel & distributed processing symposium, 2003,IEEE Press. 2003.

    • Yongjian Li, Jifeng He. Formalising Verilog. Proceedings of Applied Informatics (AI 2001) IASTED International Conference, symposium 3, Softare, Acta Press. 2001.


版权所有:中国科学院软件研究所 京ICP备05046678号