CV

Education

• B.S. in Information and Computing Science, Peking University, 2017
• Ph.D in Applied Mathematics, Peking University, 2022 (Advisor: Professor Meng Sun)

Visiting experience

• Feb. 2019 - Mar. 2020: Research Assistant
  • Nanyang Technological University
  • Supervisor: Professor Yang Liu
• Aug. 2017: Research Assistant
  • Singapore University of Technology and Design
  • Supervisor: Professor Jun Sun

Publications

Reasoning about Connectors in Coq

Xiyue Zhang, Weijiang Hong, Yi Li, Meng Sun. "Reasoning about Connectors in Coq." Proceedings of International Workshop on Formal Aspects of Component Software. FACS 2016.

Capturing Stochastic and Real-time Behavior in Reo Connectors

Yi Li, Xiyue Zhang, Yuanyi Ji, Meng Sun. "Capturing Stochastic and Real-time Behavior in Reo Connectors." Proceedings of SBMF 2017.

Using Coq for Formal Modeling and Verification of Timed Connectors

Weijiang Hong, Saqib Nawaz, Xiyue Zhang, Yi Li, Meng Sun. "Using Coq for Formal Modeling and Verification of Timed Connectors." Proceedings of International Conference on Software Engineering and Formal Methods. SEFM 2017.

Towards Formal Modeling and Verification of Probabilistic Connectors in Coq

Xiyue Zhang, Meng Sun. "Towards Formal Modeling and Verification of Probabilistic Connectors in Coq." Proceedings of the 30th International Conference on Software Engineering & Knowledge Engineering. SEKE 2018.

A Relational Model for Probabilistic Connectors based on Timed Data Distribution Streams

Meng Sun, Xiyue Zhang. "A Relational Model for Probabilistic Connectors based on Timed Data Distribution Streams." Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS 2018.

Modeling and Verification of Component Connectors

Xiyue Zhang. "Modeling and Verification of Component Connectors." Proceedings of International Conference on Formal Engineering Methods. ICFEM 2018.

Safe Inputs Generation for Black-box Systems

Bai Xue, Yang Liu, Lei Ma, Xiyue Zhang, Meng Sun, Xiaofei Xie. "Safe Inputs Generation for Black-box Systems." Proceedings of the 24th International Conference on Engineering of Complex Computer Systems. ICECCS 2019.

SMT-based Modeling and Verification of Cloud Applications

Xiyue Zhang, Meng Sun. "SMT-based Modeling and Verification of Cloud Applications." Proceedings of World Congress on Services. SERVICES 2019.

Using Recurrent Neural Network to Predict Tactics for Proving Component Connector Properties in Coq

Xiyue Zhang, Yi Li, Weijiang Hong, Meng Sun. "Using Recurrent Neural Network to Predict Tactics for Proving Component Connector Properties in Coq." Proceedings of International Symposium on Theoretical Aspects of Software Engineering. TASE 2019.

A Formal Framework Capturing Real-Time and Stochastic Behavior in Connectors

Yi Li, Xiyue Zhang, Yuanyi Ji, Meng Sun. "A Formal Framework Capturing Real-Time and Stochastic Behavior in Connectors." Science of Computer Programming. vol. 177, 2019.

Reasoning about Connectors Using Coq and Z3

Xiyue Zhang, Weijiang Hong, Yi Li, Meng Sun. "Reasoning about Connectors Using Coq and Z3." Science of Computer Programming. vol. 170, 2019.

Uncertainty-Guided Testing and Robustness Enhancement for Deep Learning Systems

Xiyue Zhang. "Uncertainty-Guided Testing and Robustness Enhancement for Deep Learning Systems." Proceedings of IEEE/ACM 42nd International Conference on Software Engineering (Companion Proceedings). ICSE-Companion 2020.

Towards a Formally Verified EVM in Production Environment

Xiyue Zhang, Yi Li, Meng Sun. "Towards a Formally Verified EVM in Production Environment." Proceedings of International Conference on Coordination Languages and Models. COORDINATION 2020.

Towards Characterizing Adversarial Defects of Deep Learning Software from the Lens of Uncertainty

Xiyue Zhang, Xiaofei Xie, Lei Ma, Xiaoning Du, Qiang Hu, Yang Liu, Jianjun Zhao, Meng Sun. "Towards Characterizing Adversarial Defects of Deep Learning Software from the Lens of Uncertainty." Proceedings of the 42nd IEEE/ACM International Conference on Software Engineering. ICSE 2020.

DeepGlobal: A Global Robustness Verifiable FNN Framework

Weidi Sun, Yuteng Lu, Xiyue Zhang, Meng Sun. "DeepGlobal: A Global Robustness Verifiable FNN Framework." Proceedings of International Symposium on Dependable Software Engineering: Theories, Tools, and Applications. SETTA 2021.

Using LSTM to Predict Tactics in Coq

Xiaokun Luan, Xiyue Zhang, Meng Sun. "Using LSTM to Predict Tactics in Coq." Proceedings of the 33rd International Conference on Software Engineering & Knowledge Engineering. SEKE 2021.

Decision-Guided Weighted Automata Extraction from Recurrent Neural Networks

Xiyue Zhang, Xiaoning Du, Xiaofei Xie, Lei Ma, Yang Liu, Meng Sun. "Decision-Guided Weighted Automata Extraction from Recurrent Neural Networks." Proceedings of the AAAI Conference on Artificial Intelligence, 35(13). AAAI 2021.

DeepGlobal: A Framework for Global Robustness Verification of Feedforward Neural Networks

Weidi Sun, Yuteng Lu, Xiyue Zhang, Meng Sun. "DeepGlobal: A Framework for Global Robustness Verification of Feedforward Neural Networks." Journal of Systems Architecture. vol. 128, 2022.

Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages

Zeming Wei, Xiyue Zhang, Meng Sun. "Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages." Proceedings of the 23rd International Conference on Formal Engineering Methods. ICFEM 2022.

Towards a Unifying Logical Framework for Neural Networks

Xiyue Zhang, Xiaohong Chen, Meng Sun. "Towards a Unifying Logical Framework for Neural Networks." Proceedings of the 19th International Colloquium on Theoretical Aspects of Computings. ICTAC 2022.

kProp: Multi-Neuron Relaxation Method for Neural Network Robustness Verification

Xiaoyong Xue, Xiyue Zhang, Meng Sun. "kProp: Multi-Neuron Relaxation Method for Neural Network Robustness Verification." Proceedings of the 10th International Conference on Fundamentals of Software Engineering. FSEN 2023.

Weighted Automata Extraction and Explanation of Recurrent Neural Networks for Natural Language Tasks

Zeming Wei, Xiyue Zhang, Yihao Zhang, Meng Sun. "Weighted Automata Extraction and Explanation of Recurrent Neural Networks for Natural Language Tasks." Journal of Logical and Algebraic Methods in Programming. Volume 136, https://doi.org/10.1016/j.jlamp.2023.100907.

Provable preimage under-approximation for neural networks

Xiyue Zhang, Benjie Wang, Marta Kwiatkowska . "Provable Preimage Under-Approximation for Neural Networks." Proceedings of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024.

Teaching

Data Structure and Algorithms (in C) (2017 Fall)

Data Structure and Algorithms (in Python) (2018 Fall)

Techniques and Methods for Programming (2020 Spring)

Data Structure and Algorithms (in Python) (2020 Fall)

Computer-Aided Formal Verification (2022 Michaelmas term)

Computer-Aided Formal Verification (2023 Michaelmas term)

Service

• PC Member
  • Program Committee of CAV 2024 (Artifact Evaluation), ICFEM 2024, FACS 2024
  • Program Committee of TASE 2023
  • Program Committee of MLiSE 2021 (co-located with ECML PKDD 2021)
• Reviewer/sub-reviewer (Journal)
  • TOSEM, JCST, SCP, JSS, FCS, IEEE Transactions on Reliability
• Reviewer/sub-reviewer (Conference)
  • CAV, TACAS, AAAI, NeurIPS, ASE, CCS, ICFEM, TASE, ASIACCS, ICECCS, COORDINATION, FORMATS, SEKE, FACS