自动推理和约束求解：如何通过高效率的（回溯）搜索过程来判断给定的约束条件（条件表达式、逻辑公式）是否成立？

程序分析与软件测试：给定一段程序，如何自动地发现其中的错误（比如数组下标越界、内存泄露）；如何自动地生成一组测试用例集，以达到某些覆盖标准（比如，百分之百的语句覆盖率）？

语义Web：如何利用语义信息来提高网络搜索的精度？如何对语义描述作推理（比如判断其一致性）？

1996年被软件所聘为副研究员
1997年12月起任中国科学院计算机科学重点实验室副主任
1999年被软件所聘为研究员
2000年获博士生导师资格

在一阶逻辑公式的可满足性问题方面取得了突出成果，提出了一种具有一般性的减小搜索空间的方法，比国外同行的方法具有明显的优越性。实现的软件工具解决了不少难题，已被二十多个国家和地区的科研人员下载。据不完全统计，有关成果目前已被五十多篇国外公开发表的文献（论文、著作）所引用。

· J. Zhang and X. Wang, A constraint solver and its application to path feasibility analysis, Int’l J. of Software Engineering and Knowledge Engineering, Vol.11, No.2, 2001.
· J. Zhang, C. Xu and S.C. Cheung, Automatic generation of database instances for white-box testing, Proc. Int’l Computer Software and Applications Conference (COMPSAC), 2001.
· 张健，逻辑公式的可满足性判定 --- 方法、工具及应用，科学出版社，北京，2000。
· 张健，有限构模器的扩展及其在形式化方法中的应用，计算机学报，第23卷第2期，2000年2月，190--194页。
· J. Zhang, S.C. Cheung and S. Chanson, Stress testing of distributed multimedia software systems, Proc. FORTE/PSTV, Kluwer Academic Publishers, 1999, pp.119-133.