[日本語][中文]

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 typical problem setting is 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}\) is not limited to classic software systems---it can be instantiated to various theoretical models or real-world systems, such as hybrid systems (cyber-physical systems) and their possible extensions with AI components. The specification \(\varphi\) is usually expressed by formal logic.

Various techniques can be developed to solve the problem, including (runtime) verification and testing. 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.

Selected publications

• [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 2023) to appear.


• [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.


• [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.


• [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.

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.

Teaching

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

Visiting

• 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.
  

Professional activities

• POPL 2021 Artifact Evaluation Committee
• EMSOFT 2019, WiP Committee Member

Awards & Grants

• 2019: JSPS DC2 (Japan Society for the Promotion of Science, Research Fellowships for Young Scientists)
• 2018: "Best Paper Award" 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