[日本語][中文]

Zhenya ZHANG (张振亚)

I am an assistant professor in Intelligent Software Engineering Laboratory, Faculty of Information Science and Electrical Engineering, Kyushu University.

Research interests

In general, I am interested in quality assurance of safety-critical complex systems, via formal methods. A commonly-seen problem statement is given as follows:

given a system model \(\mathcal{M}\) and a specification \(\varphi\), show either \(\mathcal{M}\models \varphi\) or \(\mathcal{M}\not\models \varphi\).

The system \(\mathcal{M}\) includes but is not limited to classic software systems -- it can be instantiated to a wide range of abstract models and their real-world extensions, such as hybrid systems (a.k.a. Cyber-Physical Systems) and AI-based systems (e.g., autonomous driving systems). The specification \(\varphi\) can be formally expressed, using logic languages such as temporal logic.

Various techniques have been developed to solve the problem, among which I'm very interested in verification, testing and monitoring. This is where theories and applications of software science meet: we apply theories to solve real-world problems, and these real-world concerns in return enrich the theories.

Employment

• 2022.07-now: Assistant Professor, Kyushu University, Japan.
• 2021.09-2022.06: Research Fellow, Nanyang Technological University, Singapore.
• 2020.10-2021.06: Research Fellow, Kyushu University, Japan
• 2019.04-2020.09: JSPS Research Fellow DC2, Japan.
• 2017.10-2020.10: Research Assistant, ERATO MMSD Project, National Institute of Informatics
• 2015.09-2017.07: Research Assistant, State Key Laboratory of Computer Sciences, Institute of Software Chinese Academy of Sciences

Education

• 2017-2020: PhD in Informatics, National Institute of Informatics, The Graduate University for Advanced Studies (SOKENDAI), Tokyo, Japan
  • ERATO Metamathematics for Systems Design Project (ERATO MMSD Project)
  • Supervisor: Ichiro Hasuo
• 2014-2017: Master in Computer Science, Institute of Software Chinese Academy of Sciences, University of Chinese Academy of Sciences, Beijing, China
  • State Key Laboratory of Computer Science
  • Supervisor: Yu Zhang
• 2010-2014: Bachelor in Software Engineering, Northwestern Polytechnical University, Xi'an, China.

Internship

• 2019.09-2019.12: Internship at University of Waterloo, Waterloo, Ontario, Canada. Host: Prof. Krzysztof Czarnecki.
  
• 2016.10-2016.11: Internship at Royal Holloway University of London, Egham Hill, Egham, UK. Host: Prof. Zhaohui Luo.
  

Tools

• Tumb (UAV testing): participant of SBFT'24 tool competition (CPS-UAV testing track)
• ForeSee (hybrid system falsification, based on [CAV'21]): participant of ARCH-COMP'21, ARCH-COMP'22, ARCH-COMP'23
• FalStar-MCTS (hybrid system falsification, based on [EMSOFT'18]): participant of ARCH-COMP'18, ARCH-COMP'19, ARCH-COMP'20
• FalStar (hybrid system falsification, based on [QEST'19]): participant of ARCH-COMP'18, ARCH-COMP'19, ARCH-COMP'20, ARCH-COMP'21, ARCH-COMP'22, ARCH-COMP'23

Selected Publications

• [TCAD'25] Automated Generation of Benchmarks for Falsification of STL Specifications
  Yipei Yan, Deyun Lyu, Zhenya Zhang, Paolo Arcaini, Jianjun Zhao
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (to appear)


• [ECOOP'25] Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
  Guanqin Zhang, Kota Fukuda, Zhenya Zhang, Dilum Bandara, Shiping Chen, Jianjun Zhao, Yulei Sui
  39th European Conference on Object-Oriented Programming (ECOOP 2025) (to appear)


• [OOPSLA'25] Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality
  Guanqin Zhang, Zhenya Zhang, Dilum Bandara, Shiping Chen, Jianjun Zhao, Yulei Sui
  ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2025) (to appear)


• [DATE'25] Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification
  Kota Fukuda, Guanqin Zhang, Zhenya Zhang, Yulei Sui, Jianjun Zhao
  Design, Automation and Test in Europe Conference (DATE 2025) (to appear)


• [TOSEM'24] SpectAcle: Fault Localisation of AI-Enabled CPS by Exploiting Sequences of DNN Controller Inferences
  Deyun Lyu, Zhenya Zhang, Paolo Arcaini, Xiao-Yi Zhang, Fuyuki Ishikawa, Jianjun Zhao
  ACM Transactions on Software Engineering and Methodology (to appear)


• [ASE'24] LeGEND: A Top-Down Approach to Scenario Generation of Autonomous Driving Systems Assisted by Large Language Models
  Shuncheng Tang, Zhenya Zhang, Jixiang Zhou, Lei Lei, Yuan Zhou, Yinxing Xue
  39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024) 1497-1508 (ACM SIGSOFT Distinguished Paper Award)


• [FM'24] CauMon: An Informative Online Monitor for Signal Temporal Logic
  Zhenya Zhang, Jie An, Paolo Arcaini, Ichiro Hasuo
  The 26th International Symposium on Formal Methods (FM 2024) 286-304


• [GECCO'24] Search-Based Repair of DNN Controllers of AI-Enabled Cyber-Physical Systems Guided by System-Level Specifications
  Deyun Lyu, Zhenya Zhang, Paolo Arcaini, Fuyuki Ishikawa, Thomas Laurent, Jianjun Zhao
  The Genetic and Evolutionary Computation Conference (GECCO 2024) 1435-1444


• [CAV'24] Optimization-Based Model Checking for Complex STL Specifications
  Sota Sato, Jie An, Zhenya Zhang, Ichiro Hasuo
  36th International Conference on Computer-Aided Verification. (CAV 2024) 282-306


• [ISSRE'23] EvoScenario: Integrating Road Structures into Critical Scenario Generation for Autonomous Driving System Testing
  Shuncheng Tang, Zhenya Zhang, Jixiang Zhou, Yuan Zhou, Yan-Fu Li and Yinxing Xue
  The 34th International Symposium on Software Reliability Engineering. (ISSRE 2023) 309-320.


• [CAV'23] Online Causation Monitoring of Signal Temporal Logic
  Zhenya Zhang, Jie An, Paolo Arcaini, Ichiro Hasuo
  35th International Conference on Computer-Aided Verification. (CAV 2023), 62-84.


• [TOSEM'23] A Survey on Automated Driving System Testing: Landscapes and Trends
  Shuncheng Tang, Zhenya Zhang, Yi Zhang, Jixiang Zhou, Yan Guo, Shuang Liu, Shengjian Guo, Yan-Fu Li, Lei Ma, Yinxing Xue, Yang Liu
  ACM Transactions on Software Engineering and Methodology 32(5): 1-62 (2023)


• [TSE'23] FalsifAI: Falsification of AI-Enabled Hybrid Control Systems Guided by Time-Aware Coverage Criteria
  Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo, Jianjun Zhao
  IEEE Transactions on Software Engineering 49(4): 1842 - 1859 (2023)


• [TCAD'22] A Robustness-Based Confidence Measure for Hybrid System Falsification
  Toru Takisaka, Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 42(5): 1718 - 1731 (2022)


• [EMSOFT'22] Online Reset for Signal Temporal Logic Monitoring
  Zhenya Zhang, Paolo Arcaini, Xuan Xie
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 41(11): 4421-4432 (2022)
  Special issue for the International Conference on Embedded Software (EMSOFT 2022)


• [FM'21] Gaussian Process-Based Confidence Estimation for Hybrid System Falsification
  Zhenya Zhang, Paolo Arcaini
  24th International Symposium on Formal Methods (FM 2021), 330–348.


• [CAV'21] Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness
  Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo, Jianjun Zhao
  33rd International Conference on Computer-Aided Verification. (CAV 2021), 595-618.


• [NFM'21] On the Effectiveness of Signal Rescaling in Hybrid System Falsification
  Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo, Jianjun Zhao
  13th NASA Formal Methods Symposium (NFM 2021) 392-399 2021


• [EMSOFT'20] Hybrid System Falsification under (In)equality Constraints via Search Space Transformation
  Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39(11): 3674-3685 (2020)
  Special issue for the International Conference on Embedded Software (EMSOFT 2020)


• [NFM'20] Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches
  Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
  12th NASA Formal Methods Symposium (NFM 2020) 401-419 2020.


• [QEST'19] Fast Falsification of Hybrid Systems Using Probabilistically Adaptive Input
  Gidon Ernst, Sean Sedwards, Zhenya Zhang, Ichiro Hasuo
  16th International Conference on Quantitative Evaluation of Systems (QEST 2019) 165-181 2019.


• [CAV'19] Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification
  Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini
  31st International Conference on Computer-Aided Verification (CAV 2019) 401-420 2019.


• [EMSOFT'18] Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search
  Zhenya Zhang, Gidon Ernst, Sean Sedwards, Paolo Arcaini, Ichiro Hasuo
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37(11): 2894-2905 (2018)
  Special issue for the International Conference on Embedded Software (EMSOFT 2018) ("Best Paper Award" runner-up)


• [SNR'18] Time-Staging Enhancement of Hybrid System Falsification
  Gidon Ernst, Ichiro Hasuo, Zhenya Zhang and Sean Sedwards
  The 4th International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR 2018), affiliated with ETAPS 2018.

Patents

• Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
  Model verification device and model verification method
  U.S. Patent Application No. 17/456,921. (2022) [url]

Tutorials

• Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
  Hybrid System Falsification: Fundamentals and Advanced Topics
  The 25th International Symposium on Formal Methods (FM 2023) [url] [slides] [demo]

Theses

• Zhenya Zhang
  Hierarchical Optimization for Hybrid System Falsification
  PhD thesis, The Graduate University for Advanced Studies (SOKENDAI) 2020.

Talks

• Testing of Autonomous Driving Systems: Beyond Criticality.
  Shonan meeting No. 208 - Trustworthy Machine Learning System Engineering Techniques for Practical Applications. Oct. 2024


• Falsification of AI-Enabled Hybrid Systems.
  Shonan meeting No. 204 – DevOps for CPS. Nov. 2023

Teaching

• 2025.06-08: Computer Programming Exercise (Python)
  Summer semester, 2025. Kyushu University
  


• 2025.04.21: 形式手法によるニューラルネットワーク検証
  工学概論, 2025. Kyushu University
  


• 2024.06-08: Computer Programming Exercise (Python)
  Summer semester, 2024. Kyushu University
  


• 2023.06-08: Computer Programming Exercise (Python)
  Summer semester, 2023. Kyushu University
  


• 2022.06: Hybrid System Falsification: Fundamentals and Advanced Topics.
  Gran Sasso Science Institute, Italy. PhD course. [slides]
  with Paolo Arcaini, Ichiro Hasuo.

Grants

• 反例向き、効率と保証を両立するニューラルネットワーク検証技術の開発
  Principle Investigator.
  JST BOOST (国家戦略分野の若手研究者及び博士後期課程学生の育成事業), 2025.06.01 -- 2030.05.31


• 安全な物理情報システムのための反例解釈の理論と実装
  Principle Investigator.
  Grant-in-Aid for Early-Career Scientists, 2025.04.01 –- 2028.03.31


• Testing, Analysis, and Repair of AI-Enabled Cyber-Physical Systems
  Co-Investigator.
  Grant-in-Aid for Scientific Research (B), 2023.04.01 –- 2026.03.31 [url]


• Fine-Grained Monitoring of Signal Temporal Logic and Its Applications in Quality Assurance of Cyber Physical Systems
  Principle Investigator.
  Grant-in-Aid for Early-Career Scientists, 2023.04.01 –- 2025.03.31 [url]


• 形式手法とヒューリスティクスの組み合わせによる物理情報システムの効率的な品質保証
  Principle Investigator.
  Grant-in-Aid for JSPS Fellows, 2019.04.25 -- 2021.03.31 [url]

Professional activities

Event Organizer

• Co-Organizer of verification mentoring workshop at 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA 2024)
• Program Co-Chair of the 1st International Workshop on Advanced Intelligent Software Applications (AISQ 2024)
• Registration Chair of the 27th ACM International Systems and Software Product Line Conference (SPLC 2023)

Program Committee

• The 27th International Symposium on Formal Methods (FM 2026)
• The 26th International Conference on Formal Engineering Methods (ICFEM 2025)
• 18th International Conference on the Quality of Information and Communications Technology (QUATIC 2025)
• 中国软件大会形式化方法与应用论坛 The 10th National Conference on Formal Methods and Applications (FMAC 2025)
• 19th Theoretical Aspects of Software Engineering Conference (TASE 2025)
• ACM SIGBED International Conference on Embedded Software (EMSOFT 2024)
• 25th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2024)
• 中国软件大会形式化方法与应用论坛 The 9th National Conference on Formal Methods and Applications (FMAC 2024)
• 4th International Workshop on Artificial Intelligence in Software Testing (AIST 2024)
• 17th International Conference on the Quality of Information and Communications Technology (QUATIC 2024)
• The 3rd International Workshop on Dependable Computing for Complex Systems (DCCS 2024)
• 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021) – Artifact Evaluation Committee
• ACM SIGBED International Conference on Embedded Software (EMSOFT 2019) – Program Committee of Work-in-Progress (WiP) Track

Awards

• 2024: ACM SIGSOFT Distinguished Paper Award at ASE'24.
• 2024: 2nd rank among 8 teams in UAV Testing Competition, held by SBFT'24@ICSE'24.
• 2018: "Best Paper Award" (3/42) nominee, EMSOFT 2018, Turin, Italy.
• 2011&2012: National Scholarship, China

Contact

• Email: zhang [dot] zhenya [dot] 623 [at] m.kyushu-u.ac.jp
• Email: choshina4 [at] gmail [dot] com