性别：男
职称：高级工程师
电子邮件：liujian@iscas.ac.cn
所在部门：基础软件国家工程研究中心
通讯地址：北京市海淀区中关村南四街4号（北京8718信箱）中国科学院软件研究所
电话号码：无
邮政编码： 100190
研究方向/领域：程序的分析与验证、软件自动分析和测试技术、系统软件的可信与安全
-
2000-2005 中国科学院软件研究所 博士研究生
2005-2007 中国科学院软件研究所 助理研究员
2007-现在 中国科学院软件研究所 高级工程师
-
作为课题负责人承担"访问验证级安全操作系统的安全保证技术研究"（中科院知识创新工程项目）和"高等级安全操作系统的形式化保证技术研究"（软件所计算机科学国家重点实验室开放课题）。作为研究骨干参加了多项国家、中国科学院及地方科技攻关项目，包括："传值并发系统的模型语义与验证工具"（国家自然科学基金重点项目）、"方德高可信服务器操作系统研发及产业化"（国家科技重大专项"核高基"项目）、"安全系统软件产业化"（国家发展和改革委员会产业化项目）、"国产基础软件平台体系研制及示范应用"（"十五"国家科技攻关计划重大项目）、"访问验证保护级安全操作系统原型系统研发"（中科院知识创新工程项目）、"软件并行开发技术及其CASE 系统研究"（云南省自然科学基金项目）、云南省中青年学术和技术带头人培养基金资助项目"软件工程方向"等多项科研项目。
-
[1] Qiuping Yi, Jian Liu and Wuwei Shen,?Efficient Loop-Extended Model Checking of Complex Data Structure Properties, (ASEA'2011)
[2] Wuwei Shen, Dae-Kyoo, Jian Liu, Chen Zhao,?Supporting Flexibile Reification of Design Patterns,?(APSEC'2010)
[3] Sunlv Wang, Jian Liu, Qiuping Yi and Jun Yan,?Model Checking a Secure Hypervisor,?(WCSE'2010)
[4] 刘剑，林惠民. 传值进程模型检测中诊断信息的生成，软件学报，2003，14(01):1-9；
[5] 刘剑，林惠民. 传值进程模型检测中诊断信息的生成，软件学报，2003，14(01):1-9；
[6] 刘剑，林惠民. 谓词?演算和模态图的语义一致性, 软件学报，2003，14(09):31-35；
[7] Liu Jian, Diagnose Model Checking for Value-passing CCS, In Proc. of the Automated Technology for Verification and Analysis(ATVA'2003), 2003；
[8] 和伟民，李彤，刘剑，金钊. 交互式环境下基于层次分解的并行变换技术，计算机研究与发展，1999，36(6):705-711；
[9] 刘剑，李彤. 一种并发软件规约方法的框架.计算机科学，2000，27(7):85-87；
[10] 刘剑，李彤. 一种并发系统的规约方法.计算机应用研究，2000，17(5):15-17；