[日本語][中文]
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
- 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.
Selected publications
A full list can be found at my Google scholar profile.
-
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 41(11): 4421-4432 (2022)
Special issue for the International Conference on Embedded Software (EMSOFT 2022)
-
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, 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
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
last update: 2022.Jul.2