在科技部“973”计划、国家重点研发计划、国家自然科学基金重大研究计划和优秀青年基金等项目的资助下，取得了长足的发展，发表高水平论文200余篇，包括CCF A类期刊TSE、TOSEM、TKDE、TCAD，CCF A类会议ICSE、ASE、IJCAI，理论计算机著名国际期刊TCS等数十篇，授权专利30余项，软件著作权8项，于2014年获得陕西省科技进步一等奖1项，2015年获得教育部自然科学一等奖1项，2019年获批陕西省重点创新团队。研究成果处于国内领先水平，部分研究成果国际领先，在国家“探月工程三期月地高速再入返回飞行器”和浏览器安全验证中得到了成功应用。在学术交流方面，研究所广泛开展与美国（德克萨斯大学达拉斯分校）、英国（牛津大学）、日本（法政大学）、新加坡（南洋理工大学）、航天五院五〇二所、华为等著名大学与科研机构的学术交流与合作。此外，还承办了一系列国际和国内学术会议（TASE 2011、ICFEM 2017、COCOON 2019，SOFL+MSVL 2011-2019），这些合作活动与学术交流对扩大研究所在国际上的影响，提高学术水平，拓宽研究领域和了解前沿研究动态等发挥了较大作用。

人才称号：

田聪

2019年 教育部“长江学者”特聘教授

团队获奖：

2019年 陕西省科技创新团队

项目获奖：

[1] 2015年获得陕西省科学技术奖一等奖，可信软件设计开发与验证的基础理论与关键技术，省部级

[2] 2016年获得教育部自然科学奖一等奖，程序验证的基础理论研究，省部级

期刊论文列表：

[1] Dekui Wang, Zhenhua Duan, Cong Tian, Bohu Huang, Nan Zhang:ParRA: A Shared Memory Parallel FPGA Router Using Hybrid Partitioning Approach. IEEE Trans. on CAD of Integrated Circuits and Systems 39(4): 830-842 (2020)

[2] Cong Tian, Chu Chen, Zhenhua Duan, Liang Zhao:Differential Testing of Certificate Validation in SSL/TLS Implementations: An RFC-guided Approach. ACM Trans. Softw. Eng. Methodol. 28(4): 24:1-24:37 (2019)

[3] Dekui Wang, Zhenhua Duan, Cong Tian, Bohu Huang, Nan Zhang: A Runtime Optimization Approach for FPGA Routing. IEEE Trans. on CAD of Integrated Circuits and Systems 37(8): 1706-1710 (2018)

[4] Xu Lu, Cong Tian, Zhenhua Duan, Hongwei Du: Planning with Spatio-Temporal Search Control Knowledge. IEEE Trans. Knowl. Data Eng. 30(10): 1915-1928 (2018)

[5] Cong Tian, Zhao Duan, Zhenhua Duan, C.-H. Luke Ong: More effective interpolations in software model checking. ASE 2017: 183-193

[6] Nan Zhang, Zhenhua Duan, Cong Tian: Model checking concurrent systems with MSVL. Sci. China Inf. Sci. 59(11): 118101 (2016)

[7] Ya Shi, Cong Tian, Zhenhua Duan, Mengchu Zhou: Model checking Petri nets with MSVL. Inf. Sci. 363: 274-291 (2016)

A类会议论文列表：

[1] Cong Tian, Wensheng Wang, Zhenhua Duan: Making Streett Determinization Tight. LICS 2020: 859-872

[2] Jie Zhang, Cong Tian, Zhenhua Duan: FastDroid: efficient taint analysis for Android applications. ICSE (Companion Volume) 2019: 236-237

[3] Cong Tian, Zhao Duan, Zhenhua Duan: Accelerating counterexample detection in software model checking. ICSE (Companion Volume) 2018: 250-251

[4] Cong Tian, Congli Xia, Zhenhua Duan:Android inter-component communication analysis with intent revision. ICSE (Companion Volume) 2018: 254-255

[5] Chu Chen, Cong Tian, Zhenhua Duan, Liang Zhao: RFC-directed differential testing of certificate validation in SSL/TLS implementations. ICSE 2018: 859-870

[6] Meng Wang, Cong Tian, Zhenhua Duan:Full regular temporal property verification as dynamic program execution. ICSE (Companion Volume) 2017: 226-228

[7] Xu Lu, Cong Tian, Zhenhua Duan:Temporalising Separation Logic for Planning with Search Control Knowledge. IJCAI 2017: 1167-1173

[8] Yao Liu, Zhenhua Duan, Cong Tian: A Decision Procedure for a Fragment of Linear Time Mu-Calculus. IJCAI 2016: 1195-1201