Some Publications

• Fuqi Jia, Yuhang Dong, Minghao Liu, Pei Huang, Feifei Ma, Jian Zhang. Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning. Proc. NeurIPS 2023.
• Fuqi Jia, Rui Han, Pei Huang, Minghao Liu, Feifei Ma, Jian Zhang. Improving Bit-Blasting for Nonlinear Integer Constraints. Proc. ISSTA 2023, pp.14-25.
• Changwen Li, Joseph Sifakis, Qiang Wang, Rongjie Yan, Jian Zhang. Simulation-Based Validation for Autonomous Driving Systems. Proc. ISSTA 2023, pp.842-853.
• Minghao Liu, Rui Han, Fuqi Jia, Pei Huang, Feifei Ma, Hantao Zhang, Jian Zhang. Investigating the Existence of Holey Latin Squares via Satisfiability Testing. Proc. PRICAI (2) 2023, pp.410-422.
• Suyue Guo, Xinyu Wan, Wei You, Bin Liang, Wenchang Shi, Yiwei Zhang, Jianjun Huang, Jian Zhang. Operand-Variation-Oriented Differential Analysis for Fuzzing Binding Calls in PDF Readers. Proc. ICSE 2023, pp.95-107.
• Hao Zhang, Ji Luo, Mengze Hu, Jun Yan, Jian Zhang, Zongyan Qiu. Detecting Exception Handling Bugs in C++ Programs. Proc. ICSE 2023, pp.1084-1095.
• Xi Deng, Jiwei Yan, Shixin Zhang, Jun Yan, Jian Zhang. Variable-strength combinatorial testing of exported activities based on misexposure prediction. J. Systems & Software, 204: 111773 (2023).
• Baoquan Cui, Miaomiao Wang, Chi Zhang, Jiwei Yan, Jun Yan, Jian Zhang. Detection of Java Basic Thread Misuses Based on Static Event Analysis. Proc. ASE 2023, pp.1049-1060.
• Xutong Ma, Jiwei Yan, Hao Zhang, Jun Yan, Jian Zhang. Detecting Memory Errors in Python Native Code by Tracking Object Lifecycle with Reference Count. Proc. ASE 2023, pp.1429-1440.
• Fuqi Jia, Rui Han, Xutong Ma, Baoquan Cui, Minghao Liu, Pei Huang, Feifei Ma, Jian Zhang. PSMT: Satisfiability Modulo Theories Meets Probability Distribution. Proc. ASE 2023, pp.1756-1760.
• Minghao Liu, Kunhang Lv, Pei Huang, Rui Han, Fuqi Jia, Yu Zhang, Feifei Ma, Jian Zhang. NRAgo: Solving SMT(NRA) Formulas with Gradient-Based Optimization. Proc. ASE 2023, pp.2046-2049.
• Rong Qu, Jiangang Huang, Long Zhang, Tianlu Qiao, Jian Zhang. Scope-based Compiler Differential Testing. Proc. QRS 2023, pp.360-369.
• Pei Huang, Yuting Yang, Fuqi Jia, Minghao Liu, Feifei Ma, Jian Zhang. Word Level Robustness Enhancement: Fight Perturbation with Perturbation. Proc. AAAI 2022, pp.10785-10793.
• Pei Huang, Yuting Yang, Minghao Liu, Fuqi Jia, Feifei Ma, Jian Zhang. ε-weakened robustness of deep neural networks. Proc. ISSTA 2022, pp.126-138.
• Xiaohui Zhang, Yuanjun Gong, Bin Liang, Jianjun Huang, Wei You, Wenchang Shi, Jian Zhang. Hunting bugs with accelerated optimal graph vertex matching. Proc. ISSTA 2022, pp.64-76.
• Jiwei Yan, Shixin Zhang, Yepang Liu, Xi Deng, Jun Yan, Jian Zhang. A Comprehensive Evaluation of Android ICC Resolution Techniques. Proc. ASE 2022, pp.1:1-1:13.
• Jiwei Yan, Shixin Zhang, Yepang Liu, Jun Yan, Jian Zhang. ICCBot: Fragment-Aware and Context-Sensitive ICC Resolution for Android Applications. Proc. ICSE-Companion 2022, pp.105-109.
• Miaomiao Wang, Baoquan Cui, Jiwei Yan, Jun Yan, Jian Zhang. String Test Data Generation for Java Programs. Proc. ISSRE 2022, pp.251-262.
• Jing Su, Zhen Zhang, Peng Wu, Xuran Li, Jian Zhang. Adversarial Input Detection Based on Critical Transformation Robustness. Proc. ISSRE 2022, pp.390-401.
• Xin Zhang, Rongjie Yan, Jiwei Yan, Baoquan Cui, Jun Yan, Jian Zhang. ExcePy: A Python Benchmark for Bugs with Python Built-in Types. Proc. SANER 2022, pp.856-866.
• Xutong Ma, Jiwei Yan, Wei Wang, Jun Yan, Jian Zhang, Zongyan Qiu. Detecting memory-related bugs by tracking heap memory management of C++ smart pointers. Proc. ASE 2021, pp.880-891.
• Pei Huang, Rundong Li, Minghao Liu, Feifei Ma, Jian Zhang. Efficient SAT-based minimal model generation methods for modal logic S5. Proc. SAT 2021, LNCS 12831, pp.225-241.
• Jiwei Jin, Yiqi Lv, Cunjing Ge, Feifei Ma, Jian Zhang. Investigating the Existence of Costas Latin Squares via Satisfiability Testing. Proc. SAT 2021, LNCS 12831, pp.270-279.
• Jiwei Yan, Hao Zhou, Xi Deng, Ping Wang, Rongjie Yan, Jun Yan, Jian Zhang. Efficient testing of GUI applications by event sequence reduction. Science of Computer Programming, Vol. 201: 102522 (2021).
• Xin Zhang, Jiwei Yan, Baoquan Cui, Jun Yan, Jian Zhang. Are the Scala Checks Effective? Evaluating Checks with Real-world Projects. Proc. QRS 2021, pp.978-989.
• Linjie Pan, Baoquan Cui, Hao Liu, Jiwei Yan, Siqi Wang, Jun Yan, Jian Zhang. Static asynchronous component misuse detection for Android applications. Proc. ESEC/SIGSOFT FSE 2020, pp.952-963.
• Pan Bian, Bin Liang, Jianjun Huang, Wenchang Shi, Xidong Wang, Jian Zhang. SinkFinder: harvesting hundreds of unknown interesting function pairs with just one seed. Proc. ESEC/SIGSOFT FSE 2020, pp.1101-1113.
• Minghao Liu, Fan Zhang, Pei Huang, Shuzi Niu, Feifei Ma, Jian Zhang. Learning the satisfiability of pseudo-Boolean problem with graph neural networks. Proc. CP 2020, pp.885-898.
• Jiwei Yan, Hao Liu, Linjie Pan, Jun Yan, Jian Zhang, Bin Liang. Multiple-entry testing of Android applications by constructing activity launching contexts. Proc. ICSE 2020, pp.457-468.

• Tianyong Wu, Xi Deng, Jun Yan, Jian Zhang. Analyses for specific defects in android applications: a survey. Frontiers of Computer Science, 13(6): 1210-1227 (2019)
• Xutong Ma, Jiwei Yan, Yaqi Li, Jun Yan, Jian Zhang. SPrinter: A static checker for finding smart pointer errors in C++ programs. Proc. ASE 2019, pp.1122-1125.
• Pei Huang, Minghao Liu, Ping Wang, Wenhui Zhang, Feifei Ma, Jian Zhang. Solving the satisfiability problem of modal logic S5 guided by graph coloring. Proc. IJCAI 2019, pp.1093-1100.
• Cunjing Ge, Feifei Ma, Xutong Ma, Fan Zhang, Pei Huang, Jian Zhang. Approximating integer solution counting via space quantification for linear constraints. Proc. IJCAI 2019, pp.1697-1703.
• Linjie Pan, Baoquan Cui, Jiwei Yan, Xutong Ma, Jun Yan, Jian Zhang. Androlic: an extensible flow, context, object, field, and path-sensitive static analysis framework for Android. Proc. ISSTA 2019, pp.394-397.
• Pei Huang, Minghao Liu, Cunjing Ge, Feifei Ma, Jian Zhang. Investigating the existence of orthogonal golf designs via satisfiability testing. Proc. ISSAC 2019, pp.203-210.
• Cunjing Ge, Feifei Ma, Peng Zhang, Jian Zhang. Computing and estimating the volume of the solution space of SMT(LA) constraints. Theoretical Computer Science, Vol.743, pp.110-129 (2018).
• Hongliang Liang, Xiaoxiao Pei, Xiaodong Jia, Wuwei Shen, Jian Zhang. Fuzzing: State of the Art. IEEE Trans. on Reliability, 67(3): 1199-1218 (2018).
• Jiwei Yan, Xi Deng, Ping Wang, Tianyong Wu, Jun Yan, Jian Zhang. Characterizing and identifying misexposed activities in Android applications. Proc. ASE 2018, pp.691-701.
• Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, Xutong Ma. A new probabilistic algorithm for approximate model counting. Proc. IJCAR 2018, pp.312-328.
• Pei Huang, Feifei Ma, Cunjing Ge, Jian Zhang, Hantao Zhang. Investigating the existence of large sets of idempotent quasigroups via satisfiability testing. Proc. IJCAR 2018, pp.354-369.
• Long Zhang, Lanfei Yan, Zhenyu Zhang, Jian Zhang, W. K. Chan, Zheng Zheng. A theoretical analysis on cloning the failed test cases to improve spectrum-based fault localization. Journal of Systems & Software, Vol.129, pp.35-57 (2017).
• Linjie Pan, Ji-Wei Jin, Xin Gao, Wei Sun, Feifei Ma, Minghao Yin, Jian Zhang. Integrating ILP and SMT for Shortwave Radio Broadcast Resource Allocation and Frequency Assignment. Proc. CP 2017, pp.405-413.
• Jierui Liu, Tianyong Wu, Xi Deng, Jun Yan, Jian Zhang. InsDal: A Safe and Extensible Instrumentation Tool on Dalvik Byte-code for Android Applications. Proc. SANER 2017 (tool track): 502-506.
• Tianyong Wu, Jierui Liu, Zhenbo Xu, Chaorong Guo, Yanli Zhang, Jun Yan, Jian Zhang. Light-weight, Inter-procedural and Callback-aware Resource Leak Detection for Android Apps. IEEE Transactions on Software Engineering, 42(11):1054 - 1076. Nov. 2016. (extended version of the ASE 2013 paper)
• Yan Cai, Jian Zhang, Lingwei Cao, Jian Liu. A deployable sampling strategy for data race detection. Proc. FSE 2016, pp.810-821.
• Jierui Liu, Tianyong Wu, Jun Yan and Jian Zhang. Fixing resource leaks in Android apps with light-weight static analysis and low-overhead instrumentation. Proc. ISSRE 2016, pp.342-352.
• Feifei Ma, Xin Gao, Minghao Yin, Linjie Pan, Ji-Wei Jin, Hai Liu, Jian Zhang. Optimizing shortwave radio broadcast resource allocation via pseudo-Boolean constraint solving and local search. Proc. CP 2016, pp.650-665.
• Tianyong Wu, Jierui Liu, Xi Deng, Jun Yan, and Jian Zhang. Relda2: An effective static analysis tool for resource leak detection in Android apps. Proc. ASE 2016, pp.762-767.
• Zhenbo Xu, Jian Zhang, Zhongxing Xu. Melton: a practical and precise memory leak detection tool for C programs. Frontiers of Computer Science, 9(1): 34-54, 2015. (extended version of the APSEC 2011 paper).
• Zhiqiang Zhang, Tianyong Wu, Jian Zhang. Boundary value analysis in automatic white-box test generation. Proc. ISSRE 2015, pp.239-249.
• Jian Zhang, Zhiqiang Zhang, Feifei Ma. Automatic Generation of Combinatorial Test Data. Springer, 2014.
  ISBN: 978-3-662-43428-4 (Print) 978-3-662-43429-1 (Online)
• Zhiqiang Zhang, Jun Yan, Yong Zhao, Jian Zhang. Generating combinatorial test suite using combinatorial optimization. Journal of Systems & Software, Vol.98, pp.191-207 (2014).
• Zhenbo Xu, Jian Zhang, Zhongxing Xu, Jiteng Wang. Canalyze: a static bug-finding tool for C programs. Proc. ISSTA 2014, pp.425-428.
• Tianyong Wu, Jun Yan, Jian Zhang. Automatic test data generation for unit testing to achieve MC/DC criterion. Proc. SERE 2014, pp.118-126.
• Chaorong Guo, Jian Zhang, Jun Yan, Zhiqiang Zhang, Yanli Zhang. Characterizing and detecting resource leaks in Android applications. Proc. ASE 2013, pp.389-398.
• Jian Zhang. Performance estimation using symbolic data. LNCS 8051, pp.346-353, 2013.
• Hantao Zhang, Jian Zhang. MACE4 and SEM: A comparison of finite model generators. LNCS 7788, pp.101-130, 2013.
• Jian Zhang, Feifei Ma, Zhiqiang Zhang. Faulty interaction identification via constraint solving and optimization. Proc. SAT 2012, LNCS 7317, pp.186-199.
• Feifei Ma, Jun Yan, Jian Zhang. Solving generalized optimization problems subject to SMT constraints. Proc. FAW/AAIM 2012, LNCS 7285, pp.247-258.
• Runming Lu, Sheng Liu, Jian Zhang. Searching for doubly self-orthogonal Latin squares. Proc. CP 2011, pp.538-545.
• Zhiqiang Zhang, Jian Zhang. Characterizing failure-causing parameter interactions by adaptive testing. Proc. ISSTA 2011, pp.331-341.
• Sheng Liu, Jian Zhang. Program analysis: from qualitative analysis to quantitative analysis (NIER track). Proc. ICSE 2011, pp.956-959.
• Baiqiang Chen, Jian Zhang. Tuple density: a new metric for combinatorial test suites (NIER track). Proc. ICSE 2011, pp.876-879.
• Baiqiang Chen, Jian Zhang. Combinatorial testing with shielding parameters. Proc. APSEC 2010, pp.280-289.
• Zhongxing Xu, Ted Kremenek, Jian Zhang. A memory model for static analysis of C programs. Proc. ISoLA 2010, Part I, LNCS 6415, pp.535-548.

• Feifei Ma, Sheng Liu, Jian Zhang. Volume computation for Boolean combination of linear arithmetic constraints. Proc. CADE-22, LNCS 5663, pp.453-468, 2009.
• Jun Yan, Jian Zhang. An efficient method to generate feasible paths for basis path testing. Information Processing Letters, 107(3-4): 87-92, 2008.
• Jun Yan, Jian Zhang. A backtracking search tool for constructing combinatorial test suites. Journal of Systems & Software, 81(10): 1681-1693, 2008.
• Zhongxing Xu, Jian Zhang. Path and context sensitive inter-procedural memory leak detection. Proc. QSIC 2008, pp.412-420.
• Hui Ruan, Jian Zhang, Jun Yan. Test data generation for C programs with string-handling functions. Proc. TASE 2008, pp.219-226.
• Feifei Ma, Jian Zhang. Finding orthogonal arrays using satisfiability checkers and symmetry breaking constraints. Proc. PRICAI 2008, LNCS 5351, pp.247-259.
• Jian Zhang. Constraint solving and symbolic execution. Proc. VSTTE 2005, LNCS 4171, pp.539-544, 2008.
• Sheng Liu, Jian Zhang, Binhai Zhu. Volume computation using a direct Monte Carlo method. Proc. COCOON 2007, LNCS 4598, pp.198-209.
• Jun Yan, Zhong Jie Li, Yuan Yuan, Wei Sun, Jian Zhang. BPEL4WS unit testing: Test case generation using a concurrent path analysis approach. Proc. ISSRE 2006, pp.75-84.
• Zhongxing Xu, Jian Zhang. A test data generation tool for unit testing of C programs. Proc. QSIC 2006, pp.107-116.
• Xiangxue Jia, Jian Zhang. A powerful technique to eliminate isomorphism in finite model search. Proc. IJCAR 2006, LNCS 4130, pp.318-331.
• Jian Zhang, Chen Xu, Xiaoliang Wang. Path-oriented test data generation using symbolic execution and constraint solving techniques. Proc. SEFM 2004, pp.242-250.
• Jian Zhang. Symbolic execution of program paths involving pointer and structure variables. Proc. QSIC 2004, pp.87-92.
• Jian Zhang. Quantitative Analysis of Symbolic Execution. Proc. COMPSAC 2004, pp.184-185.
• Jian Zhang, Chen Xu, S.-C. Cheung. Automated test case generation for the stress testing of multimedia systems. Software - Practice and Experience, 32(15): 1411-1435 (2002).
• Wenhui Zhang, Zhuo Huang, Jian Zhang. Parallel execution of stochastic search procedures on reduced SAT instances. Proc. PRICAI 2002, LNCS(LNAI) Vol. 2417, pp.108-117.
• Jian Zhang. A path-based approach to the detection of infinite looping. Proc. APAQS 2001, pp.88-94.
• Jian Zhang, Chen Xu, S.-C. Cheung. Automatic generation of database instances for white-box testing. Proc. COMPSAC 2001, pp.161-165.
• Jian Zhang, Xiaoxu Wang. A constraint solver and its application to path feasibility analysis. International Journal of Software Engineering and Knowledge Engineering, 11(2), pp.139-156.
• Jian Zhang. Specification analysis and test data generation by solving Boolean combinations of numeric constraints. Proc. APAQS 2000, pp.267-274.