A Calculus for Generic, QoS-Aware Component Composition. - Luís Soares Barbosa; Meng Sun 002 (Math. Comput. Sci., 2012)

Modeling and Analysis of Component Connectors in Coq. - Yi Li 010; Meng Sun 002 (FACS, 2013)

Formal modeling and verification of complex interactions in e-government applications. - Meng Sun 002; Yi Li 010 (ICEGOV, 2014)

A Hybrid Model of Connectors in Cyber-Physical Systems. - Xiaohong Chen 002; Jun Sun 001; Meng Sun 002 (ICFEM, 2014)

A Framework for Off-Line Conformance Testing of Timed Connectors. - Shaodong Li; Xiaohong Chen 002; Yiwu Wang; Meng Sun 002 (TASE, 2015)

Modeling and verification of component connectors in Coq. - Yi Li 010; Meng Sun 002 (Sci. Comput. Program., 2015)

Reasoning About Connectors in Coq. - Xiyue Zhang 001; Weijiang Hong; Yi Li 010; Meng Sun 002 (FACS, 2016)

Towards Concolic Testing for Hybrid Systems. - Pingfan Kong; Yi Li 010; Xiaohong Chen 002; Jun Sun 001; Meng Sun 002; Jingyi Wang 004 (FM, 2016)

Active Learning from Blackbox to Timed Connectors. - Yi Li 010; Meng Sun 002; Yiwu Wang (TASE, 2016)

Component-Based Modeling in Mediator. - Yi Li 010; Meng Sun 002 (FACS, 2017)

Capturing Stochastic and Real-Time Behavior in Reo Connectors. - Yi Li 010; Xiyue Zhang 001; Yuanyi Ji; Meng Sun 002 (SBMF, 2017)

Using Coq for Formal Modeling and Verification of Timed Connectors. - Weijiang Hong; M. Saqib Nawaz; Xiyue Zhang 001; Yi Li 010; Meng Sun 002 (SEFM Workshops, 2017)

A Formal Design Model for Genetic Algorithms Operators and its Encoding in PVS. - M. Saqib Nawaz; Meng Sun 002 (BDIOT, 2018)

Generating Arduino C Codes from Mediator. - Yi Li 010; Meng Sun 002 (It's All About Coordination, 2018)

A Relational Model for Probabilistic Connectors Based on Timed Data Distribution Streams. - Meng Sun 002; Xiyue Zhang 001 (FORMATS, 2018)

Modeling and Verification of IEEE 802.11i Security Protocol for Internet of Things. - Yuteng Lu; Meng Sun 002 (SEKE, 2018)

Reo2PVS: Formal Specification and Verification of Component Connectors. - M. Saqib Nawaz; Meng Sun 002 (SEKE, 2018)

Towards Formal Modeling and Verification of Probabilistic Connectors in Coq (S). - Xiyue Zhang 001; Meng Sun 002 (SEKE, 2018)

On Semantics for Mediator: A Coalgebraic Perspective. - Ai Liu; Shun Wang; Yi Li 010; Meng Sun 002 (SOFL+MSVL, 2018)

Modeling and Verification of IEEE 802.11i Security Protocol in UPPAAL for Internet of Things. - Yuteng Lu; Meng Sun 002 (Int. J. Softw. Eng. Knowl. Eng., 2018)

A Formal Specification and Verification Framework for Timed Security Protocols. - Li Li 044; Jun Sun 001; Yang Liu 003; Meng Sun 002; Jin Song Dong (IEEE Trans. Software Eng., 2018)

Using PVS for Modeling and Verification of Probabilistic Connectors. - M. Saqib Nawaz; Meng Sun 002 (FSEN, 2019)

Proof Guidance in PVS with Sequential Pattern Mining. - M. Saqib Nawaz; Meng Sun 002; Philippe Fournier-Viger (FSEN, 2019)

Safe Inputs Approximation for Black-Box Systems. - Bai Xue; Yang Liu 003; Lei Ma 003; Xiyue Zhang 001; Meng Sun 002; Xiaofei Xie (ICECCS, 2019)

A Coalgebraic Semantics Framework for Quantum Systems. - Ai Liu; Meng Sun 002 (ICFEM, 2019)

PRISM Code Generation for Verification of Mediator Models (S). - Weidi Sun; Meng Sun 002 (SEKE, 2019)

SMT-Based Modeling and Verification of Cloud Applications. - Xiyue Zhang 001; Meng Sun 002 (SERVICES, 2019)

Distributed Mediator. - Yi Li 010; Meng Sun 002 (TASE, 2019)

Using Recurrent Neural Network to Predict Tactics for Proving Component Connector Properties in Coq. - Xiyue Zhang 001; Yi Li 010; Weijiang Hong; Meng Sun 002 (TASE, 2019)

A Survey on Theorem Provers in Formal Methods. - M. Saqib Nawaz; Moin Malik; Yi Li 010; Meng Sun 002; Muhammad Ikram Ullah Lali (CoRR, 2019)

A formal framework capturing real-time and stochastic behavior in connectors. - Yi Li 010; Xiyue Zhang 001; Yuanyi Ji; Meng Sun 002 (Sci. Comput. Program., 2019)

Reasoning about connectors using Coq and Z3. - Xiyue Zhang 001; Weijiang Hong; Yi Li 010; Meng Sun 002 (Sci. Comput. Program., 2019)

Modeling and Verification of the Nervos CKB Block Synchronization Protocol in UPPAAL. - Qi Zhang; Yuteng Lu; Meng Sun 002 (BlockSys, 2020)

Towards a Formally Verified EVM in Production Environment. - Xiyue Zhang 001; Yi Li 010; Meng Sun 002 (COORDINATION, 2020)

Towards Modeling and Verification of the CKB Block Synchronization Protocol in Coq. - Hao Bu; Meng Sun 002 (ICFEM, 2020)

Towards characterizing adversarial defects of deep learning software from the lens of uncertainty. - Xiyue Zhang 001; Xiaofei Xie; Lei Ma 003; Xiaoning Du 001; Qiang Hu; Yang Liu 003; Jianjun Zhao 001; Meng Sun 002 (ICSE, 2020)

Proof searching in HOL4 with genetic algorithm. - Muhammad Zohaib Nawaz; Osman Hasan; M. Saqib Nawaz; Philippe Fournier-Viger; Meng Sun 002 (SAC, 2020)

Global Robustness Verification Networks. - Weidi Sun; Yuteng Lu; Xiyue Zhang 001; Zhanxing Zhu; Meng Sun 002 (CoRR, 2020)

Mediator: A component-based modeling language for concurrent and distributed systems. - Yi Li 010; Weidi Sun; Meng Sun 002 (Sci. Comput. Program., 2020)

Decision-Guided Weighted Automata Extraction from Recurrent Neural Networks. - Xiyue Zhang 001; Xiaoning Du 001; Xiaofei Xie; Lei Ma 003; Yang Liu 003; Meng Sun 002 (AAAI, 2021)

Are Coverage Criteria Meaningful Metrics for DNNs? - Weidi Sun; Yuteng Lu; Meng Sun 002 (IJCNN, 2021)

Modeling and Verification of CKB Consensus Protocol in Coq. - Xiaokun Luan; Meng Sun 002 (QRS Companion, 2021)

Modeling and Verification of CKB Consensus Protocol in UPPAAL (S). - Yi-Chun Feng; Yuteng Lu; Meng Sun 002 (SEKE, 2021)

DeepAuto: A First Step Towards Formal Verification of Deep Learning Systems (S). - Yuteng Lu; Weidi Sun; Guangdong Bai; Meng Sun 002 (SEKE, 2021)

Using LSTM to Predict Tactics in Coq. - Xiaokun Luan; Xiyue Zhang 001; Meng Sun 002 (SEKE, 2021)

Mutation Testing of Reinforcement Learning Systems. - Yuteng Lu; Weidi Sun; Meng Sun 002 (SETTA, 2021)

DeepGlobal: A Global Robustness Verifiable FNN Framework. - Weidi Sun; Yuteng Lu; Xiyue Zhang 001; Meng Sun 002 (SETTA, 2021)

Proof Searching in PVS Theorem Prover Using Simulated Annealing. - M. Saqib Nawaz; Meng Sun 002; Philippe Fournier-Viger (ICSI (2), 2021)

Proof searching and prediction in HOL4 with evolutionary/heuristic and deep learning techniques. - M. Saqib Nawaz; Muhammad Zohaib Nawaz; Osman Hasan; Philippe Fournier-Viger; Meng Sun 002 (Appl. Intell., 2021)

An evolutionary/heuristic-based proof searching framework for interactive theorem prover. - M. Saqib Nawaz; Muhammad Zohaib Nawaz; Osman Hasan; Philippe Fournier-Viger; Meng Sun 002 (Appl. Soft Comput., 2021)

A Unifying Coalgebraic Semantics Framework for Quantum Systems. - Ai Liu; Meng Sun 002 (Int. J. Softw. Eng. Knowl. Eng., 2021)

RGChaser: A RL-guided Fuzz and Mutation Testing Framework for Deep Learning Systems. - Yuteng Lu; Kaicheng Shao; Weidi Sun; Meng Sun 002 (DSA, 2022)

Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages. - Zeming Wei; Xiyue Zhang 001; Meng Sun 002 (ICFEM, 2022)

Towards a Unifying Logical Framework for Neural Networks. - Xiyue Zhang 001; Xiaohong Chen 002; Meng Sun 002 (ICTAC, 2022)

MTUL: Towards Mutation Testing of Unsupervised Learning Systems. - Yuteng Lu; Kaicheng Shao; Weidi Sun; Meng Sun 002 (SETTA, 2022)

HashC: Making DNNs' Coverage Testing Finer and Faster. - Weidi Sun; Xiaoyong Xue; Yuteng Lu; Meng Sun 002 (SETTA, 2022)

EPMC Gets Knowledge in Multi-agent Systems. - Chen Fu; Ernst Moritz Hahn; Yong Li 031; Sven Schewe; Meng Sun 002; Andrea Turrini; Lijun Zhang 001 (VMCAI, 2022)

Quality of service in IoT protocol as designs and its verification in PVS. - Muhammad Saqib Nawaz; Meng Sun 002; Basit Shahzad; Muhammad Ikram Ullah Lali; Tariq Umer; Shaohua Wan 001 (Trans. Emerg. Telecommun. Technol., 2022)

Probabilistic mediator: A coalgebraic perspective. - Ai Liu; Shaoying Liu; Meng Sun 002 (J. Log. Algebraic Methods Program., 2022)

Towards mutation testing of Reinforcement Learning systems. - Yuteng Lu; Weidi Sun; Meng Sun 002 (J. Syst. Archit., 2022)

DeepGlobal: A framework for global robustness verification of feedforward neural networks. - Weidi Sun; Yuteng Lu; Xiyue Zhang 001; Meng Sun 002 (J. Syst. Archit., 2022)

kProp: Multi-neuron Relaxation Method for Neural Network Robustness Verification. - Xiaoyong Xue; Xiyue Zhang 001; Meng Sun 002 (FSEN, 2023)

Guiding the Comparison of Neural Network Local Robustness: An Empirical Study. - Hao Bu; Meng Sun 002 (ICANN (5), 2023)

Certifying Semantic Robustness of Deep Neural Networks. - Hao Bu; Meng Sun 002 (ICECCS, 2023)

Branch and Bound for Sigmoid-Like Neural Network Verification. - Xiaoyong Xue; Meng Sun 002 (ICFEM, 2023)

DeepPatch: A Patching-Based Method for Repairing Deep Neural Networks. - Hao Bu; Meng Sun 002 (DeepTest, 2023)

Measuring Robustness of Deep Neural Networks from the Lens of Statistical Model Checking. - Hao Bu; Meng Sun 002 (IJCNN, 2023)

MedTiny: Enhanced Mediator Modeling Language for Scalable Parallel Algorithms. - Xiangyu Li; Yihao Zhang; Xiaokun Luan; Xiaoyong Xue; Meng Sun 002 (QRS Companion, 2023)

Using Z3 for Formal Modeling and Verification of FNN Global Robustness (S). - Yihao Zhang; Zeming Wei; Xiyue Zhang 001; Meng Sun 002 (SEKE, 2023)

HeatC: A Variable-Grained Coverage Criterion for Deep Learning Systems. - Weidi Sun; Yuteng Lu; Xiaokun Luan; Meng Sun 002 (SETTA, 2023)

Using Z3 for Formal Modeling and Verification of FNN Global Robustness. - Yihao Zhang; Zeming Wei; Xiyue Zhang 001; Meng Sun 002 (CoRR, 2023)

HashC: Making deep learning coverage testing finer and faster. - Weidi Sun; Xiaoyong Xue; Yuteng Lu; Jia Zhao; Meng Sun 002 (J. Syst. Archit., 2023)

Optimal Solution Guided Branching Strategy for Neural Network Branch and Bound Verification. - Xiaoyong Xue; Meng Sun 002 (ICECCS, 2024)

Adversarial Representation Engineering: A General Model Editing Framework for Large Language Models. - Yihao Zhang; Zeming Wei; Jun Sun 001; Meng Sun 002 (NeurIPS, 2024)

MILE: A Mutation Testing Framework of In-Context Learning Systems. - Zeming Wei; Yihao Zhang; Meng Sun 002 (SETTA, 2024)

Towards General Conceptual Model Editing via Adversarial Representation Engineering. - Yihao Zhang; Zeming Wei; Jun Sun 001; Meng Sun 002 (CoRR, 2024)

Automata Extraction from Transformers. - Yihao Zhang; Zeming Wei; Meng Sun 002 (CoRR, 2024)

Protecting Deep Learning Model Copyrights with Adversarial Example-Free Reuse Detection. - Xiaokun Luan; Xiyue Zhang 001; Jingyi Wang 004; Meng Sun 002 (CoRR, 2024)

The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap. - Yedi Zhang; Yufan Cai; Xinyue Zuo; Xiaokun Luan; Kailong Wang 001; Zhe Hou; Yifan Zhang; Zhiyuan Wei; Meng Sun 002; Jun Sun 001; Jing Sun 002; Jin Song Dong (CoRR, 2024)

Weighted automata extraction and explanation of recurrent neural networks for natural language tasks. - Zeming Wei; Xiyue Zhang 001; Yihao Zhang; Meng Sun 002 (J. Log. Algebraic Methods Program., 2024)

Mutation testing of unsupervised learning systems. - Yuteng Lu; Kaicheng Shao; Jia Zhao; Weidi Sun; Meng Sun 002 (J. Syst. Archit., 2024)

Clopper-Pearson Algorithms for Efficient Statistical Model Checking Estimation. - Hao Bu; Meng Sun 002 (IEEE Trans. Software Eng., 2024)

MedTiny Code Generation for Enhancing RegLang Smart Contract Reliability. - Xiaokun Luan; Yihao Zhang; Meng Sun 002 (SAC, 2025)

Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs. - Ziyun Xu; Hao Wang 002; Meng Sun 002 (TASE, 2025)

Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle. - Xiaokun Luan; David Sanán; Zhe Hou; Qiyuan Xu; Chengwei Liu; Yufan Cai; Yang Liu 003; Meng Sun 002 (Proc. ACM Softw. Eng., 2025)

Robust and Efficient Watermarking of Large Language Models Using Error Correction Codes. - Xiaokun Luan; Zeming Wei; Yihao Zhang; Meng Sun 002 (Proc. Priv. Enhancing Technol., 2025)

Runtime Backdoor Detection for Federated Learning via Representational Dissimilarity Analysis. - Xiyue Zhang 001; Xiaoyong Xue; Xiaoning Du 001; Xiaofei Xie; Yang Liu 003; Meng Sun 002 (IEEE Trans. Dependable Secur. Comput., 2025)