[日本語][中文]
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
- 2014-2017: Master in Computer Science,
Institute of Software Chinese Academy of Sciences,
University of Chinese Academy of Sciences, Beijing, China
- 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), ranked 2nd among 8 teams
-
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
Publications
see also my [Google scholar] profile
Journal Papers
-
[KBS'24]
On the Effectiveness of Graph Data Augmentation for Source Code Learning
Zeming Dong, Qiang Hu, Zhenya Zhang, Jianjun Zhao
Knowledge-Based Systems. Volume 285 (2024) (IF: 8.8, CORE B)
-
[PR'23]
TAT: Targeted Backdoor Attacks against Visual Object Tracking
Ziyi Cheng, Baoyuan Wu, Zhenya Zhang and Jianjun Zhao
Pattern Recognition. Volume 142, 15 pages. (IF: 8, CORE A*)
-
[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) (CORE A*)
-
[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 and Yang Liu
ACM Transactions on Software Engineering and Methodology 32(5): 1-62 (2023) (CORE A*)
-
[TCAD'23]
A Robustness-Based Confidence Measure for Hybrid System Falsification
Toru Takisaka, Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
IEEE Trans. on CAD of Integrated Circuits and Systems 42(5): 1718 - 1731 (2023) (CCF A)
-
[EMSOFT'22]
Online Reset for Signal Temporal Logic Monitoring
Zhenya Zhang, Paolo Arcaini, Xuan Xie
IEEE Trans. on CAD of Integrated Circuits and Systems 41(11): 4421-4432 (2022)
Special issue for the International Conference on Embedded Software (EMSOFT 2022) (CORE A)
-
[TOMACS'21]
Falsification of Hybrid Systems Using Adaptive Probabilistic Search
Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo
ACM Transactions on Modeling and Computer Simulation (TOMACS) 31, no. 3 (2021): 1-22. (CORE B)
-
[EMSOFT'20]
Hybrid System Falsification under (In)equality Constraints via Search Space Transformation
Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
IEEE Trans. on CAD of Integrated Circuits and Systems 39(11): 3674-3685 (2020)
Special issue for the International Conference on Embedded Software (EMSOFT 2020) (CORE A)
-
[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 Trans. on CAD of Integrated Circuits and Systems 37(11): 2894-2905 (2018)
Special issue for the International Conference on Embedded Software (EMSOFT 2018) (CORE A) ("Best Paper Award" runner-up)
-
[IJSEKE'17]
Localization of Linearizability Faults on the Coarse-Grained Level.
Zhenya Zhang, Peng Wu, and Yu Zhang.
International Journal of Software Engineering and Knowledge Engineering 27, no. 09n10 (2017): 1483-1505. (CORE B)
Extended version of SEKE'17
International Conferences
-
[SBFT'24]
TUMB at the SBFT 2024 Tool Competition –- CPS-UAV Test Case Generation Track
Shuncheng Tang, Zhenya Zhang, Ahmet Cetinkaya, Paolo Arcaini
The 17th Intl. Workshop on Search-Based and Fuzz Testing (SBFT'24), affiliated with ICSE'24 to appear
- [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 34rd International Symposium on Software Reliability Engineering. (ISSRE'23) 309-320. (CORE A)
-
[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. (CORE A*)
-
[QRS-C'23]
Boosting Source Code Learning with Text-Oriented Data Augmentation: An Empirical Study
Zeming Dong, Qiang Hu, Yuejun Guo, Zhenya Zhang, and Jianjun Zhao
23rd IEEE International Conference Software Quality, Reliability, and Security Companion (QRS-C'23) 383-392 (2023)
-
[ARCH'23]
ARCH-COMP 2023 Category Report: Falsification
Claudio Menghi, Paolo Arcaini, Walstan Baptista, Gidon Ernst, Georgios Fainekos, Federico Formica, Sauvik Gon, Tanmay Khandait, Atanu Kundu, Giulia Pedrielli, Jarkko Peltomäki, Ivan Porres, Rajarshi Ray, Masaki Waga, Zhenya Zhang
10th International Workshop on Applied Verification of Continuous and Hybrid Systems. (ARCH'23), 151-169
-
[SANER'23]
MixCode: Enhancing Code Classification by Mixup-Based Data Augmentation
Zeming Dong, Qiang Hu, Yuejun Guo, Maxime Cordy, Mike Papadakis, Zhenya Zhang, Yves Le Traon and Jianjun Zhao
IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER’23) 379-390. (2023). (CORE A)
-
[ICSE-SEIP'22]
When Cyber-Physical Systems Meet AI: A Benchmark, an Evaluation, and a Way Forward.
Jiayang Song, Deyun Lyu, Zhenya Zhang, Zhijie Wang, Tianyi Zhang, and Lei Ma.
International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP’22), 343-352 (2022) (CORE A*)
-
[ARCH'22]
ARCH-COMP 2022 category report: Falsification with ubounded resources
Gidon Ernst, Paolo Arcaini, Georgios Fainekos, Federico Formica, Jun Inoue, Tanmay Khandait, Mohammad Mahdi Mahboob, Claudio Menghi, Giulia Pedrielli, Masaki Waga, Yoriyuki Yamagata, Zhenya Zhang
9th International Workshop on Applied Verification of Continuous and Hybrid Systems. (ARCH'22) 204-221 (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. (CORE A)
-
[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. (CORE A*)
-
[ARCH'21]
ARCH-COMP 2021 Category Report: Falsification with Validation of Results.
Gidon Ernst, Paolo Arcaini, Ismail Bennani, Aniruddh Chandratre, Alexandre Donzé, Georgios Fainekos, Goran Frehse, Khouloud Gaaloul, Jun Inoue, Tanmay Khandait, Logan Mathesen, Claudio Menghi, Giulia Pedrielli, Marc Pouzet, Masaki Waga, Shakiba Yaghoubi, Yoriyuki Yamagata, Zhenya Zhang
8th International Workshop on Applied Verification of Continuous and Hybrid Systems. (ARCH'21) 133-152 (2021)
-
[RADAS'21]
Issue Categorization and Analysis of an Open-Source Driving Assistant System.
Shuncheng Tang, Zhenya Zhang, Jia Tang, Lei Ma, and Yinxing Xue.
International Workshop on Reliability of Advanced Driving Assistant System, co-located at ISSRE’21 148-153. (2021)
-
[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
-
[ARCH'20]
ARCH-COMP 2020 Category Report: Falsification
Gidon Ernst, Paolo Arcaini, Ismail Bennani, Alexandre Donze, Georgios Fainekos, Goran Frehse, Logan Mathesen, Claudio Menghi, Giulia Pedrinelli, Marc Pouzet, Shakiba Yaghoubi, Yoriyuki Yamagata, Zhenya Zhang
7th International Workshop on Applied Verification of Continuous and Hybrid Systems. (ARCH'20)
-
[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.
-
[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 (CORE A*)
-
[QEST'19]
Fast Falsification of Hybrid Systems Using Probabilistically Adaptive Input
Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo.
International Conference on Quantitative Evaluation of Systems (QEST’19), 165-181. (2019) (CORE A*)
-
[ARCH'19]
ARCH-COMP 2019 Category Report: Falsification.
Gidon Ernst, Paolo Arcaini, Alexandre Donze, Georgios Fainekos, Logan Mathesen, Giulia Pedrielli, Shakiba Yaghoubi, Yoriyuki Yamagata, Zhenya Zhang
6th International Workshop on Applied Verification of Continuous and Hybrid Systems. (ARCH'19) 129-140
-
[MT-CPS'19]
Hybrid System Falsification Using Monte Carlo Tree Search
Zhenya Zhang, Gidon Ernst, Sean Sedwards, Paolo Arcaini, and Ichiro Hasuo
4th Workshop on Monitoring and Testing of Cyber-Physical Systems, Part of CPS-IoT Week 2019 (MT-CPS’19) 2019.
-
[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.
-
[SETTA'18]
Interleaving-Tree Based Fine-Grained Linearizability Fault Localization.
Yang Chen, Zhenya Zhang, Peng Wu, and Yu Zhang.
International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA’18), 108-126. (2018)
-
[ARCH'18]
ARCH-COMP18 Category Report: Results on the Falsification Benchmarks
Adel Dokhanchi, Shakiba Yaghoubi, Bardh Hoxha, Georgios Fainekos, Gidon Ernst, Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo, Sean Sedwards
5th International Workshop on Applied Verification of Continuous and Hybrid Systems. (ARCH'18) 104-109
-
[MT-CPS'18]
Time-Staging Enhancement of Hybrid System Falsification (Abstract)
Zhenya Zhang, Gidon Ernst, Ichiro Hasuo, and Sean Sedwards.
IEEE Workshop on Monitoring and Testing of Cyber-Physical Systems (MT-CPS’18) 3-4. (2018)
-
[SEKE'17]
Localization of Linearizability Faults on the Coarse-Grained Level
Zhenya Zhang, Peng Wu, and Yu Zhang.
29th International Conference on Software Engineering and Knowledge Engineering (SEKE'17) 272-277. (2017) (CORE B)
Domestic Conferences
-
[JSSST'23]
Zhenya Zhang, Jie An, Paolo Arcaini and Ichiro Hasuo
Online Causation Monitoring of Signal Temporal Logic
日本ソフトウェア科学会第 40 回大会 (2023 年度) 講演論文集
-
[JSSST'22]
Zhenya Zhang and Paolo Arcaini
Gaussian Process-Based Confidence Estimation for Hybrid System Falsification.
日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集
-
[JSSST'21]
Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo and Jianjun Zhao
Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness
日本ソフトウェア科学会第 38 回大会 (2021 年度) 講演論文集
-
[JSSST'20]
Zhenya Zhang, Paolo Arcaini and Ichiro Hasuo
Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification
日本ソフトウェア科学会第 37 回大会 (2020 年度) 講演論文集
Book Chapters
-
Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
Optimisation-Based Falsification -- Showcasing Black-Box Techniques for System Safety
Chapter 1 of the book Safety Assurance under Uncertainties: from Software to Cyber-Physical/ Machine Learning Systems (to appear)
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
Talks
-
Falsification of AI-Enabled Hybrid Systems.
Shonan meeting No. 204 – DevOps for CPS. Nov. 2023
-
Falsification: From Hybrid Systems to AI Systems.
Seminar in Institute of Software Chinese Academy of Sciences. Sep. 2023
-
Stochastic Optimization-based Falsification
情報系 WINTER FESTA Episode 5, 2019年12月
-
Time-Staging Enhancement of Hybrid System Falsification
情報系 WINTER FESTA Episode3, 2017年12月
Teaching
-
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
-
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
-
Registration Chair of the 27th ACM International Systems and Software Product Line Conference (SPLC 2023)
Program Committee
-
2024:
-
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)
-
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)
-
2023:
-
The 11th International Symposium on Computing and Networking (CANDAR 2023)
-
The 2nd International Workshop on Dependable Computing for Complex Systems (DCCS 2023)
-
The 5th International Workshop on Dependable Intelligent Systems (DeIS 2023)
-
2022:
-
The Tenth International Symposium on Computing and Networking (CANDAR 2022)
-
The 1st International Workshop on Dependable Computing for Complex Systems (DCCS 2022)
-
2021:
-
The Ninth International Symposium on Computing and Networking (CANDAR 2021)
-
3rd International Workshop on Dependable Intelligent Systems (DelS 2021)
-
48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021) – Artifact Evaluation Committee
-
2019:
-
ACM SIGBED International Conference on Embedded Software (EMSOFT 2019) – Program Committee of Work-in-Progress (WiP) Track
Awards
-
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.
-
2017: MEXT Honors Scholarship, Japan
-
2017: NII Scholarship, National Institute of Informatics, Japan
-
2012: National Scholarship, China
-
2011: National Scholarship, China
Contact
- Email: zhang [dot] zhenya [dot] 623 [at] m.kyushu-u.ac.jp
- Email: choshina4 [at] gmail [dot] com