基本信息
张健  男  博导  中国科学院软件研究所
电子邮件: zj@ios.ac.cn
通信地址: 中关村南四街四号
邮政编码: 100190

研究领域

软件工程、人工智能(自动推理;约束求解;软件测试;代码静态分析)

招生信息

   
招生专业
083500-软件工程
081202-计算机软件与理论
招生方向
程序分析与软件测试
自动推理与约束求解
软件测试

教育背景

   
学历
-- 研究生
学位
-- 博士

教授课程

软件测试与分析

专利与奖励

奖励信息
(1) 王选新闻科学技术奖, 一等奖, 其他, 2017
(2) 中创软件人才奖, , 其他, 2000
专利成果
( 1 ) 基于附加测试的多参数系统错误模式快速定位方法, 发明, 2011, 第 2 作者, 专利号: 201010539469.4
( 2 ) 一种多参量软件测试方法, 发明, 2010, 第 2 作者, 专利号: 201010526993.8

出版信息

   
发表论文
[1] Jian Zhang. Efficient SAT-based Minimal Model Generation Methods for Modal Logic S5. The 24th International Conference on Theory and Applications of Satisfiability Testing. 2021, [2] yan, Jiwei, Zhou, Hao, Deng, Xi, Wang, Ping, Yan, Rongjie, Yan, Jun, Zhang, Jian. Efficient testing of GUI applications by event sequence reduction. SCIENCE OF COMPUTER PROGRAMMING[J]. 2021, 201: http://dx.doi.org/10.1016/j.scico.2020.102522.
[3] Jian Zhang. Investigating the Existence of Costas Latin Squares via Satisfiability Testing. The 24th International Conference on Theory and Applications of Satisfiability Testing. 2021, [4] Chen, Guozhu, Zeng, Fanping, Zhang, Jian, Lu, Tingting, Shen, Jingfei, Shu, Wenjuan. An adaptive trust model based on recommendation filtering algorithm for the Internet of Things systems. COMPUTER NETWORKS[J]. 2021, 190: http://dx.doi.org/10.1016/j.comnet.2021.107952.
[5] Deng, Xi, Zhang, Zhiqiang, Li, Rundong, Yan, Jun, Zhang, Jian. Combinatorial Testing of Browsers' Support for Multimedia. IEEE TRANSACTIONS ON RELIABILITY[J]. 2020, 69(4): 1323-1340, https://www.webofscience.com/wos/woscc/full-record/WOS:000595526500009.
[6] Jian Zhang. SinkFinder: Harvesting Hundreds of Unknown Interesting Function Pairs with Just One Seed. ESEC/FSE. 2020, [7] Zhang, Long, Li, Zijie, Feng, Yang, Zhang, Zhenyu, Chan, Wing Kwong, Zhang, Jian, Zhou, Yuming. Improving Fault-Localization Accuracy by Referencing Debugging History to Alleviate Structure Bias in Code Suspiciousness. IEEE TRANSACTIONS ON RELIABILITY[J]. 2020, 69(3): 1021-1049, https://www.webofscience.com/wos/woscc/full-record/WOS:000566336900014.
[8] Jian Zhang. Static Asynchronous Component Misuse Detection for Android Applications. FSE. 2020, [9] Jian Zhang. Multiple-Entry Testing of Android Applications by Constructing Activity Launching Contexts. ICSE. 2020, [10] Jian Zhang. Learning the Satisfiability of Pseudo-Boolean Problem with Graph Neural Networks. The 26th International Conference on Principles and Practice of Constraint Programming. 2020, [11] Wu, Tianyong, Deng, Xi, Yan, Jun, Zhang, Jian. Analyses for specific defects in android applications: a survey. FRONTIERS OF COMPUTER SCIENCEnull. 2019, 13(6): 1210-1227, https://www.webofscience.com/wos/woscc/full-record/WOS:000475801700005.
[12] 吕成成, 张龙, 邓茜, 曾凡平, 严俊, 张健. Web应用程序搜索功能的组合测试. 计算机科学与探索[J]. 2019, 13(11): 1839-1851, http://lib.cqvip.com/Qikan/Article/Detail?id=7100165602.
[13] Jian Zhang. Reorganizing and Optimizing Post-Inspection on Suspicious Bug Reports in Path-Sensitive Analysis. QRS. 2019, [14] Lv Chengcheng, Zhang Long, Zeng Fanping, Zhang Jian, IEEE. Adaptive Random Testing for XSS Vulnerability. 2019 26TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC)null. 2019, 63-69, [15] 张健, 张超, 玄跻峰, 熊英飞, 王千祥, 梁彬, 李炼, 窦文生, 陈振邦, 陈立前, 蔡彦. 程序分析研究进展. 软件学报. 2019, 30(1): 80-109, http://lib.cqvip.com/Qikan/Article/Detail?id=7001388130.
[16] Jian Zhang. Approximating Integer Solution Counting via Space Quantification for Linear Constraints. IJCAI. 2019, [17] Liu, Yepang, Wang, Jue, Wei, Lili, Xu, Chang, Cheung, ShingChi, Wu, Tianyong, Yan, Jun, Zhang, Jian. DroidLeaks: a comprehensive database of resource leaks in Android apps. EMPIRICAL SOFTWARE ENGINEERING[J]. 2019, 24(6): 3435-3483, https://www.webofscience.com/wos/woscc/full-record/WOS:000501131100007.
[18] Huang, Pei, Liu, Minghao, Ge, Cunjing, Ma, Feifei, Zhang, Jian, ACM. Investigating the Existence of Orthogonal Golf Designs via Satisfiability Testing. PROCEEDINGS OF THE 2019 ACM INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC '19)null. 2019, 203-210, http://dx.doi.org/10.1145/3326229.3326232.
[19] Jian Zhang. SPrinter: A Static Checker for Finding Smart Pointer Errors in C++ Programs. ASE. 2019, [20] Jian Zhang. Solving the Satisfiability Problem of Modal Logic S5 Guided by Graph Coloring. The 28th International Joint Conference on Artificial Intelligence. 2019, [21] Pan Linjie, Cui Baoquan, Yan Jiwei, Ma Xutong, Yan Jun, Zhang Jian, Zhang DM, Moller A. Androlic: An Extensible Flow, Context, Object, Field, and Path-Sensitive Static Analysis Framework for Android. PROCEEDINGS OF THE 28TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS (ISSTA '19)null. 2019, 394-397, http://dx.doi.org/10.1145/3293882.3339001.
[22] Bereg, Sergey, Ma, Feifei, Wang, Wencheng, Zhang, Jian, Zhu, Binhai. On some matching problems under the color-spanning model. THEORETICAL COMPUTER SCIENCE[J]. 2019, 786: 26-31, http://dx.doi.org/10.1016/j.tcs.2018.08.008.
[23] Liang, Hongliang, Pei, Xiaoxiao, Jia, Xiaodong, Shen, Wuwei, Zhang, Jian. Fuzzing: State of the Art. IEEE TRANSACTIONS ON RELIABILITY[J]. 2018, 67(3): 1199-1218, https://www.webofscience.com/wos/woscc/full-record/WOS:000443970200032.
[24] 张健, 王海峰, 张文辉, 董威, 徐宝文. 安全攸关软件系统及其质量保障. 科技纵览. 2018, 68-69, http://lib.cqvip.com/Qikan/Article/Detail?id=676232538.
[25] Ge Cunjing, Ma Feifei, Liu Tian, Zhang Jian, Ma Xutong, Galmiche D, Schulz S, Sebastiani R. A New Probabilistic Algorithm for Approximate Model Counting. AUTOMATED REASONING, IJCAR 2018null. 2018, 10900: 312-328, [26] Ge, Cunjing, Yan, Jiwei, Yan, Jun, Zhang, Jian, Sun, J, Sun, M. Checking Activity Transition Systems with Back Transitions Against Assertions. FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2018null. 2018, 11232: 388-403, [27] Yan, Jiwei, Pan, Linjie, Li, Yaqi, Yan, Jun, Zhang, Jian, Assoc Comp Machinery. LAND: A User-Friendly and Customizable Test Generation Tool for Android Apps. ISSTA'18: PROCEEDINGS OF THE 27TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSISnull. 2018, 360-363, http://dx.doi.org/10.1145/3213846.3229500.
[28] Ge, Cunjing, Ma, Feifei, Zhang, Peng, Zhang, Jian. Computing and estimating the volume of the solution space of SMT(LA) constraints. THEORETICAL COMPUTER SCIENCE[J]. 2018, 743: 110-129, https://www.webofscience.com/wos/woscc/full-record/WOS:000444661700010.
[29] Yang Ling, Yan Jun, Zhang Jian, Assoc Comp Machinery. Generating Minimal Test Set Satisfying MC/DC Criterion via SAT Based Approach. 33RD ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTINGnull. 2018, 1899-1906, http://dx.doi.org/10.1145/3167132.3167335.
[30] Yan, Jiwei, Deng, Xi, Wang, Ping, Wu, Tianyong, Yan, Jun, Zhang, Jian, Huchard, M, Kastner, C, Fraser, G. Characterizing and Identifying Misexposed Activities in Android Applications. PROCEEDINGS OF THE 2018 33RD IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMTED SOFTWARE ENGINEERING (ASE' 18)null. 2018, 691-701, [31] Huang Pei, Ma Feifei, Ge Cunjing, Zhang Jian, Zhang Hantao, Galmiche D, Schulz S, Sebastiani R. Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing. AUTOMATED REASONING, IJCAR 2018null. 2018, 10900: 354-369, [32] Pan, Linjie, Jin, Jiwei, Gao, Xin, Sun, Wei, Ma, Feifei, Yin, Minghao, Zhang, Jian, Beck, JC. Integrating ILP and SMT for Shortwave Radio Broadcast Resource Allocation and Frequency Assignment. PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING (CP 2017)null. 2017, 10416: 405-413, [33] Deng, Xi, Wu, Tianyong, Yan, Jun, Zhang, Jian, IEEE. Combinatorial Testing on Implementations of HTML5 Support. 10TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION WORKSHOPS - ICSTW 2017null. 2017, 262-271, [34] Zhang, Long, Yan, Lanfei, Zhang, Zhenyu, Zhang, Jian, Chan, W K, Zheng, Zheng. A theoretical analysis on cloning the failed test cases to improve spectrum-based fault localization. JOURNAL OF SYSTEMS AND SOFTWARE[J]. 2017, 129: 35-57, http://dx.doi.org/10.1016/j.jss.2017.04.017.
[35] Yan, Jiwei, Wu, Tianyong, Yan, Jun, Zhang, Jian, IEEE. Widget-Sensitive and Back-Stack-Aware GUI Exploration for Testing Android Apps. 2017 IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS)null. 2017, 42-53, http://dx.doi.org/10.1109/QRS.2017.14.
[36] Jian Zhang. Symbolic Execution with Value-range Analysis for Floating-point Exception Detection. 24th Asia-Pacific Software Engineering Conference (APSEC'17). 2017, [37] Lu, Xian, Shang, Yun, Lu, Ruqian, Zhang, Jian, Ma, Feifei. Weak QMV algebras and some ring-like structures. SOFT COMPUTING[J]. 2017, 21(10): 2537-2547, https://www.webofscience.com/wos/woscc/full-record/WOS:000400234600010.
[38] 燕季薇, 黄晓伟, 严俊, 张健, 杨红丽. 基于Android平台的黑盒测试生成工具的研究对比. 计算机应用与软件. 2017, 34(8): 1-6, http://lib.cqvip.com/Qikan/Article/Detail?id=672752798.
[39] Yan Dong, Pan Linjie, Yan Rongjie, Yan Jun, Zhang Jian, Reisman S, Ahamed SI, Demartini C, Conte T, Liu L, Claycomb W, Nakamura M, Tovar E, Cimato S, Lung CH, Takakura H, Yang JJ, Akiyama T, Zhang Z, Hasan K. Comprehensive Static Analysis for Configurable Software via Combinatorial Instantiation. 2017 IEEE 41ST ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1null. 2017, 67-74, [40] Liu Jierui, Wu Tianyong, Deng Xi, Yan Jun, Zhang Jian, Pinzger M, Bavota G, Marcus A. InsDal: A Safe and Extensible Instrumentation Tool on Dalvik Byte-Code for Android Applications. 2017 IEEE 24TH INTERNATIONAL CONFERENCE ON SOFTWARE ANALYSIS, EVOLUTION, AND REENGINEERING (SANER)null. 2017, 502-506, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000402557000059.
[41] 杨红丽, 姜皓, 秦胜潮, 张健, 严俊. Android应用能耗漏洞分析技术综述. 计算机应用与软件. 2016, 33(9): 1-6, http://lib.cqvip.com/Qikan/Article/Detail?id=670036516.
[42] Wu Tianyong, Liu Jierui, Deng Xi, Yan Jun, Zhang Jian, Lo D, Apel S, Khurshid S. Relda2: An Effective Static Analysis Tool for Resource Leak Detection in Android Apps. 2016 31ST IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE)null. 2016, 762-767, [43] Wu, Tianyong, Liu, Jierui, Xu, Zhenbo, Guo, Chaorong, Zhang, Yanli, Yan, Jun, Zhang, Jian. Light-Weight, Inter-Procedural and Callback-Aware Resource Leak Detection for Android Apps. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING[J]. 2016, 42(11): 1054-1076, https://www.webofscience.com/wos/woscc/full-record/WOS:000388866100004.
[44] Wu Xingming, Xu Zhenbo, Yan Dong, Wu Tianyong, Yan Jun, Zhang Jian, Potanin A, Murphy GC, Reeves S, Dietrich J. The Floating-point Extension of Symbolic Execution Engine for Bug Detection. 2016 23RD ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2016)null. 2016, 265-272, [45] Jian Zhang. Optimizing Shortwave Radio Broadcast Resource Allocation via Pseudo-Boolean Constraint Solving and Local Search. The 22nd International Conference on Principles and Practice of Constraint Programming. 2016, [46] Liu Jierui, Wu Tianyong, Yan Jun, Zhang Jian, IEEE. Fixing Resource Leaks in Android Apps with Light-weight Static Analysis and Low-overhead Instrumentation. 2016 IEEE 27TH INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING (ISSRE)null. 2016, 342-352, [47] Jian Zhang. A deployable sampling strategy for data race detection. Proc. FSE. 2016, [48] 金继伟, 马菲菲, 张健. SMT求解技术简述. 计算机科学与探索[J]. 2015, 9(7): 769-780, http://lib.cqvip.com/Qikan/Article/Detail?id=665316953.
[49] Xu, Zhenbo, Zhang, Jian, Xu, Zhongxing. Melton: a practical and precise memory leak detection tool for C programs. FRONTIERS OF COMPUTER SCIENCE[J]. 2015, 9(1): 34-54, https://www.webofscience.com/wos/woscc/full-record/WOS:000348798400003.
[50] Jian Zhang. Boundary Value Analysis in Automatic White-box Test Generation. Proc. ISSRE. 2015, [51] Jian Zhang. Canalyze: a static bug-finding tool for C programs. Proc. ISSTA 2014. 2014, [52] Zhang, Zhiqiang, Yan, Jun, Zhao, Yong, Zhang, Jian. Generating combinatorial test suite using combinatorial optimization. JOURNAL OF SYSTEMS AND SOFTWARE[J]. 2014, 98: 191-207, http://dx.doi.org/10.1016/j.jss.2014.09.001.
[53] Wu Tianyong, Yan Jun, Zhang Jian, IEEE. Automatic Test Data Generation for Unit Testing to Achieve MC/DC Criterion. 2014 EIGHTH INTERNATIONAL CONFERENCE ON SOFTWARE SECURITY AND RELIABILITYnull. 2014, 118-126, [54] Hu Yan, Yan Jun, Zhang Jian, Jiang He. Profile directed systematic testing of concurrent programs. 2013 8th International Workshop on Automation of Software Test, AST 2013null. 2013, 47-52, http://ir.iscas.ac.cn/handle/311060/16652.
[55] Zhao Yong, Zhang Zhiqiang, Yan Jun, Zhang Jian. Cascade: a Test Generation Tool for Combinatorial Testing. IEEE SIXTH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION WORKSHOPS (ICSTW 2013)null. 2013, 267-270, [56] 赵勇, 张智强, 严俊, 张健. 软件兼容性测试的故障定位分析. 计算机科学与探索. 2013, 7(5): 405-411, http://lib.cqvip.com/Qikan/Article/Detail?id=45852031.
[57] Ma FeiFei, Zhang Jian. Finding orthogonal latin squares using finite model searching tools. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2013, 56(3): https://www.webofscience.com/wos/woscc/full-record/WOS:000318197000012.
[58] Guo Chaorong, Zhang Jian, Yan Jun, Zhang Zhiqiang, Zhang Yanli, IEEE. Characterizing and Detecting Resource Leaks in Android Applications. 2013 28TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE)null. 2013, 389-398, [59] Wu Tianyong, Yan Jun, Zhang Jian. A path-oriented approach to generating executable test sequences for extended finite state machines. Proceedings - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012null. 2012, 267-270, http://ir.iscas.ac.cn/handle/311060/15750.
[60] Ma Feifei, Yan Jun, Zhang Jian. Solving generalized optimization problems subject to smt constraints. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)null. 2012, 247-258, http://ir.iscas.ac.cn/handle/311060/15733.
[61] Zhang Jian, Ma Feifei, Zhang Zhiqiang. Faulty interaction identification via constraint solving and optimization. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)null. 2012, 186-199, http://ir.iscas.ac.cn/handle/311060/15773.
[62] Jin, JiWei, Ma, FeiFei, Zhang, Jian. Integrating Standard Dependency Schemes in QCSP Solvers. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY[J]. 2012, 27(1): 37-41, http://lib.cqvip.com/Qikan/Article/Detail?id=40704184.
[63] Zhang Zhiqiang, Liu Xiaojian, Zhang Jian. Combinatorial testing on id3v2 tags of mp3 files. Proceedings - IEEE 5th International Conference on Software Testing, Verification and Validation, ICST 2012null. 2012, 587-590, http://ir.iscas.ac.cn/handle/311060/15715.
[64] Zhang, Xinchang, Yang, Meihong, Zhang, Jian, Shi, Huiling, Zhang, Wei. A study on the extended unique input/output sequence. INFORMATION SCIENCES[J]. 2012, 203: 44-58, http://dx.doi.org/10.1016/j.ins.2012.03.007.
[65] 金继伟, 马菲菲, 张健. Integrating Standard Dependency Schemes in QCSP Solvers. 计算机科学技术学报:英文版. 2012, 27(1): 37-41, http://lib.cqvip.com/Qikan/Article/Detail?id=40704184.
[66] Liu Sheng, Zhang Jian, IEEE. Program Analysis: From Qualitative Analysis to Quantitative Analysis (NIER Track). 2011 33RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE)null. 2011, 956-959, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000297156400123.
[67] Xu Zhenbo, Zhang Jian, Xu Zhongxing. Memory Leak Detection Based On Memory State Transition Graph. 2011 18TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2011)null. 2011, 33-40, [68] Chen Baiqiang, Zhang Jian. Tuple density: a new metric for combinatorial test suites (nier track). Proceedings - International Conference on Software Engineeringnull. 2011, 876-879, http://124.16.136.157/handle/311060/14209.
[69] Chen Baiqiang, Yan Jun, Zhang Jian. Combinatorial testing with shielding parameters. Proceedings - Asia-Pacific Software Engineering Conference, APSECnull. 2010, 280-289, http://124.16.136.157/handle/311060/8692.
[70] Xu Zhongxing, Kremenek Ted, Zhang Jian, Margaria T, Steffen B. A Memory Model for Static Analysis of C Programs. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT Inull. 2010, 6415: 535-+, [71] 严俊, 张健. 组合测试:原理与方法. 软件学报. 2009, 1393-1405, http://lib.cqvip.com/Qikan/Article/Detail?id=30626092.
[72] 阮辉, 严俊, 张健. 基于路径分析的死循环检测. 计算机学报. 2009, 1750-1758, http://lib.cqvip.com/Qikan/Article/Detail?id=31573016.
[73] Ji Xiaohui, Ma Feifei, Zhang Jian, Miao H, Hu G. Solving Global Unconstrained Optimization Problems by Symmetry-Breaking. PROCEEDINGS OF THE 8TH IEEE/ACIS INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION SCIENCEnull. 2009, 107-+, http://dx.doi.org/10.1109/ICIS.2009.66.
[74] Ma Feifei, Liu Sheng, Zhang Jian, Schmidt RA. Volume Computation for Boolean Combination of Linear Arithmetic Constraints. AUTOMATED DEDUCTION - CADE-22null. 2009, 5663: 453-468, [75] 张健. 精确的程序静态分析. 计算机学报. 2008, 31(9): 1549-1553, http://lib.cqvip.com/Qikan/Article/Detail?id=28228229.
[76] Zhang Jian, Zhang Wenhui, Zhan Naijun, Shen Yidong, Chen Haiming, Zhang Yunquan, Wang Yongji, Wu Enhua, Wang Hongan, Zhu Xueyang. Basic research in computer science and software engineering at sklcs. Frontiers of Computer Science in China[J]. 2008, 2(1): 1-11, [77] Yan, Jun, Zhang, Jian. An efficient method to generate feasible paths for basis path testing. INFORMATION PROCESSING LETTERS[J]. 2008, 107(3-4): 87-92, https://www.webofscience.com/wos/woscc/full-record/WOS:000257531300001.
[78] 徐贵红, 张健. 语义网的一阶逻辑推理技术支持. 软件学报. 2008, 19(12): 3091-3099, http://lib.cqvip.com/Qikan/Article/Detail?id=28816350.
[79] Yan, Jun, Zhang, Jian. A backtracking search tool for constructing combinatorial test suites. JOURNAL OF SYSTEMS AND SOFTWARE[J]. 2008, 81(10): 1681-1693, http://dx.doi.org/10.1016/j.jss.2008.02.034.
[80] 陈云霁, 张健, 沈海华, 胡伟武. 一种基于SAT的运算电路查错方法. 计算机学报. 2007, 30(12): 2082-2089, http://lib.cqvip.com/Qikan/Article/Detail?id=26098706.
[81] 季晓慧, 张健. 约束问题求解. 自动化学报. 2007, 33(2): 125-131, http://lib.cqvip.com/Qikan/Article/Detail?id=23811290.
[82] 徐贵红, 张健. 基于约束的主动规则终止性分析. 计算机研究与发展. 2006, 43(5): 894-900, http://lib.cqvip.com/Qikan/Article/Detail?id=21816494.
[83] 季晓慧, 张健. 一种求解混合约束问题的快速完备算法. 计算机研究与发展. 2006, 43(3): 551-556, http://lib.cqvip.com/Qikan/Article/Detail?id=21356792.
[84] Zhang Jian, Ji XIaohui. 求解布尔与非线性数值约束相混合的约束问题. 软件学报. 2005, 16(5): 659-668, http://lib.cqvip.com/Qikan/Article/Detail?id=15677466.
[85] 季晓慧, 黄拙, 张健. 约束求解与优化技术的结合. 计算机学报. 2005, 28(11): 1790-1797, http://lib.cqvip.com/Qikan/Article/Detail?id=20636526.
[86] 季晓慧, 张健. 求解布尔与非线性数值约束相混合的约束问题. 软件学报. 2005, 16(5): 659-668, http://lib.cqvip.com/Qikan/Article/Detail?id=15677466.
[87] 李韶华, 张健. Survey Propagation:一种求解SAT的高效算法. 计算机科学. 2005, 32(1): 132-137, http://lib.cqvip.com/Qikan/Article/Detail?id=12050395.
[88] Zhang Jian, Huang Zhuo. 由一阶逻辑公式得到命题逻辑可满足性问题实例. 软件学报. 2005, 16(3): 327-335, http://lib.cqvip.com/Qikan/Article/Detail?id=15052072.
[89] 吴萍, 陈意云, 张健. 并发Java程序同步操作的有效删除. 软件学报. 2005, 16(10): 1708-1716, http://lib.cqvip.com/Qikan/Article/Detail?id=20256546.
[90] 杨宇, 张健. 程序静态分析技术与工具. 计算机科学. 2004, 31(2): 171-174, http://lib.cqvip.com/Qikan/Article/Detail?id=9323003.
[91] 张健. 有限构模器的扩展及其在形式化方法中的应用. 计算机学报. 2000, 23(2): 190-194, http://lib.cqvip.com/Qikan/Article/Detail?id=4138446.
[92] 张健. —一阶逻辑中约束求解的局部搜索法. 软件学报. 1998, 9(8): 598-600, http://lib.cqvip.com/Qikan/Article/Detail?id=3276429.
[93] 张健. 模态逻辑推理的翻译方法. 计算机研究与发展. 1998, 35(5): 389-392, http://lib.cqvip.com/Qikan/Article/Detail?id=3023911.
[94] 张健. Automatic construction of finite algebras. Journal of Computer Science and Technology[J]. 1995, 10(3): 206-213, http://lib.cqvip.com/Qikan/Article/Detail?id=6853499.
[95] 张健. 有限模型生成及其应用. 1994, 52-, http://ir.iscas.ac.cn/handle/311060/6242.
[96] 张健. 数学对象的计算机搜索. 自然杂志. 1992, 215-219, http://lib.cqvip.com/Qikan/Article/Detail?id=1005171315.
发表著作
(1) 逻辑公式的可满足性判定--方法、工具及应用, Deciding the Satisfiability of Logical Formulas -- Methods, Tools and Applications, 科学出版社, 2000-10, 第 1 作者
(2) 组合测试数据自动生成, Automatic Generation of Combinatorial Test Data, Springer, 2014-09, 第 1 作者

科研活动

   
科研项目
( 1 ) 安全攸关软件系统的构造与质量保障方法研究, 主持, 国家级, 2014-01--2018-08
( 2 ) 软件安全性分析的关键技术与工具, 主持, 国家级, 2015-01--2016-12
( 3 ) 大规模软件的自动化分析与测试, 主持, 部委级, 2017-05--2022-05

指导学生

已指导学生

徐贵红  博士研究生  081202-计算机软件与理论  

严俊  博士研究生  081202-计算机软件与理论  

季晓慧  博士研究生  081202-计算机软件与理论  

李韶华  硕士研究生  081203-计算机应用技术  

石玉祥  硕士研究生  081202-计算机软件与理论  

刘生  博士研究生  081202-计算机软件与理论  

许中兴  博士研究生  081202-计算机软件与理论  

贾祥雪  博士研究生  081202-计算机软件与理论  

阮辉  硕士研究生  081202-计算机软件与理论  

陈柏强  博士研究生  081202-计算机软件与理论  

马菲菲  博士研究生  081202-计算机软件与理论  

卢闰明  硕士研究生  081202-计算机软件与理论  

赵勇  硕士研究生  081202-计算机软件与理论  

郭超容  硕士研究生  081202-计算机软件与理论  

张智强  博士研究生  081202-计算机软件与理论  

张艳丽  硕士研究生  085211-计算机技术  

葛存菁  博士研究生  081202-计算机软件与理论  

吴兴明  博士研究生  081202-计算机软件与理论  

吴添勇  博士研究生  083500-软件工程  

燕季薇  硕士研究生  083500-软件工程  

刘洁瑞  硕士研究生  085211-计算机技术  

张龙  博士研究生  081202-计算机软件与理论  

吕亦奇  硕士研究生  085211-计算机技术  

杨玲  硕士研究生  085211-计算机技术  

王平  硕士研究生  083500-软件工程  

李润东  硕士研究生  085211-计算机技术  

现指导学生

黄沛  博士研究生  081202-计算机软件与理论  

潘临杰  博士研究生  083500-软件工程  

刘明昊  博士研究生  081202-计算机软件与理论  

邓茜  博士研究生  083500-软件工程  

马旭桐  博士研究生  083500-软件工程  

刘晴  硕士研究生  085212-软件工程  

刘力铭  硕士研究生  085212-软件工程  

章新  硕士研究生  083500-软件工程  

张豪  博士研究生  081202-计算机软件与理论  

王伟  硕士研究生  085212-软件工程  

贾富琦  博士研究生  081200-计算机科学与技术  

王思琪  硕士研究生  085400-电子信息  

崔保全  博士研究生  083500-软件工程  

张丽玮  硕士研究生  083500-软件工程  

工作经历

1999年起,任中国科学院软件研究所研究员;
2000年起,任中国科学院软件研究所博士生导师。
2004年起,任《计算机学报》编委;
2010年起,任 JCST 编委、Frontiers of CS 编委。