[日本語][中文]
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)
-
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 my [Google scholar] profile for a full list
- [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 Trans. on CAD 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 Trans. on CAD 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 Trans. on CAD 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 Trans. on CAD 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
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
-
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
-
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
-
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