[日本語][中文]

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 shown 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 logics.

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

Selected publications

• Toru Takisaka, Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
  A Robustness-Based Confidence Measure for Hybrid System Falsification
  IEEE Trans. on CAD of Integrated Circuits and Systems (2022) to appear
• Zhenya Zhang, Paolo Arcaini, Xuan Xie
  Online Reset for Signal Temporal Logic Monitoring
  IEEE Trans. on CAD of Integrated Circuits and Systems
  Special issue for the International Conference on Embedded Software (EMSOFT 2022) to appear.
• Zhenya Zhang, Paolo Arcaini
  Gaussian Process-Based Confidence Estimation for Hybrid System Falsification
  24th International Symposium on Formal Methods (FM 2021), 330–348. [doi]
• Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo, Jianjun Zhao
  Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness
  33rd International Conference on Computer-Aided Verification. (CAV 2021), 595-618. [doi]
• Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo, Jianjun Zhao
  On the Effectiveness of Signal Rescaling in Hybrid System Falsification
  13th NASA Formal Methods Symposium. (NFM 2021), 392-399 [doi]
• Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
  Hybrid System Falsification under (In)equality Constraints via Search Space Transformation
  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) [doi]
• Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo
  Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches.
  12th NASA Formal Methods Symposium (NFM 2020) 401-419 2020. [doi]
• Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini
  Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification.
  31st International Conference on Computer-Aided Verification (CAV 2019) 401-420 2019. [doi]
• Zhenya Zhang, Gidon Ernst, Sean Sedwards, Paolo Arcaini, Ichiro Hasuo
  Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search
  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) [doi] (nominated as "Best Paper Award")
• Gidon Ernst, Ichiro Hasuo, Zhenya Zhang and Sean Sedwards
  Time-Staging Enhancement of Hybrid System Falsification.
  The 4th International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR 2018), affiliated with ETAPS 2018. [doi]

Tutorials

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

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