Towards an Algebraic Theory of Typed Mobile Processes. - Yuxin Deng 001; Davide Sangiorgi (ICALP, 2004)

Ensuring Termination by Typability. - Yuxin Deng 001; Davide Sangiorgi (IFIP TCS, 2004)

Compositional Reasoning for Probabilistic Finite-State Behaviors. - Yuxin Deng 001; Catuscia Palamidessi; Jun Pang 001 (Processes, Terms and Cycles, 2005)

Axiomatizations for Probabilistic Finite-State Behaviors. - Yuxin Deng 001; Catuscia Palamidessi (FoSSaCS, 2005)

Metrics for Action-labelled Quantitative Transition Systems. - Yuxin Deng 001; Tom Chothia; Catuscia Palamidessi; Jun Pang 001 (QAPL, 2005)

Weak Probabilistic Anonymity. - Yuxin Deng 001; Catuscia Palamidessi; Jun Pang 001 (SecCO@CONCUR, 2005)

Measuring Anonymity with Relative Entropy. - Yuxin Deng 001; Jun Pang 001; Peng Wu 002 (Formal Aspects in Security and Trust, 2006)

Analyzing an Electronic Cash Protocol Using Applied Pi Calculus. - Zhengqin Luo; Xiaojuan Cai; Jun Pang 001; Yuxin Deng 001 (ACNS, 2007)

Scalar Outcomes Suffice for Finitary Probabilistic Testing. - Yuxin Deng 001; Rob J. van Glabbeek; Carroll Morgan; Chenyi Zhang 001 (ESOP, 2007)

Characterising Testing Preorders for Finite Probabilistic Processes. - Yuxin Deng 001; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan; Chenyi Zhang 001 (LICS, 2007)

Probabilistic Barbed Congruence. - Yuxin Deng 001; Wenjie Du 001 (QAPL, 2007)

Remarks on Testing Probabilistic Processes. - Yuxin Deng 001; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan; Chenyi Zhang 001 (Computation, Meaning, and Logic, 2007)

Game Characterizations of Process Equivalences. - Xin Chen 002; Yuxin Deng 001 (APLAS, 2008)

On Automatic Verification of Self-Stabilizing Population Protocols. - Jun Pang 001; Zhengqin Luo; Yuxin Deng 001 (TASE, 2008)

Characterising Testing Preorders for Finite Probabilistic Processes. - Yuxin Deng 001; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan (Log. Methods Comput. Sci., 2008)

Verifying Anonymous Credential Systems in Applied Pi Calculus. - Xiangxi Li; Yu Zhang; Yuxin Deng 001 (CANS, 2009)

Testing Finitary Probabilistic Processes. - Yuxin Deng 001; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan (CONCUR, 2009)

A Local Algorithm for Checking Probabilistic Bisimilarity. - Yuxin Deng 001; Wenjie Du 001 (FCST, 2009)

The Kantorovich Metric in Computer Science: A Brief Survey. - Yuxin Deng 001; Wenjie Du 001 (QAPL, 2009)

On Mobility and Communication. - Wenjie Du 001; Yuxin Deng 001 (ISDT, 2009)

Characterising Probabilistic Processes Logically - (Extended Abstract). - Yuxin Deng 001; Rob J. van Glabbeek (LPAR (Yogyakarta), 2010)

Characterising Probabilistic Processes Logically - Yuxin Deng 001; Rob J. van Glabbeek (CoRR, 2010)

A Framework for Verifying Data-Centric Protocols. - Yuxin Deng 001; Stéphane Grumbach; Jean-François Monin (FMOODS/FORTE, 2011)

Compositional Reasoning for Markov Decision Processes - (Extended Abstract). - Yuxin Deng 001; Matthew Hennessy (FSEN, 2011)

On the Semantics of Markov Automata. - Yuxin Deng 001; Matthew Hennessy (ICALP (2), 2011)

Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation - Yuxin Deng 001; Wenjie Du 001 (CoRR, 2011)

Real-Reward Testing for Probabilistic Processes (Extended Abstract) - Yuxin Deng 001; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan (QAPL, 2011)

Open Bisimulation for Quantum Processes. - Yuxin Deng 001; Yuan Feng 001 (IFIP TCS, 2012)

Characterisations of testing preorders for a finite probabilistic π-calculus. - Yuxin Deng 001; Alwen Tiu (Formal Aspects Comput., 2012)

The Buffered π-Calculus: A Model for Concurrent Languages. - Xiaojie Deng; Yu Zhang; Yuxin Deng 001; Farong Zhong (LATA, 2013)

Compositional reasoning for weighted Markov decision processes. - Yuxin Deng 001; Matthew Hennessy (Sci. Comput. Program., 2013)

Modal Characterisations of Probabilistic and Fuzzy Bisimulations. - Yuxin Deng 001; Hengyang Wu (ICFEM, 2014)

Real-reward testing for probabilistic processes. - Yuxin Deng 001; Rob J. van Glabbeek; Matthew Hennessy; Carroll Morgan (Theor. Comput. Sci., 2014)

Symbolic Bisimulation for Quantum Processes. - Yuan Feng 001; Yuxin Deng 001; Mingsheng Ying (ACM Trans. Comput. Log., 2014)

On Coinduction and Quantum Lambda Calculi. - Yuxin Deng 001; Yuan Feng 001; Ugo Dal Lago (CONCUR, 2015)

Modal Characterisations of Behavioural Pseudometrics. - Yuxin Deng 001; Wenjie Du 001; Daniel Gebler (CoRR, 2015)

Program equivalence in linear contexts. - Yuxin Deng 001; Yu Zhang (Theor. Comput. Sci., 2015)

Behavioural Pseudometrics for Nondeterministic Probabilistic Systems. - Wenjie Du 001; Yuxin Deng 001; Daniel Gebler (SETTA, 2016)

Logical characterizations of simulation and bisimulation for fuzzy transition systems. - Hengyang Wu; Yuxin Deng 001 (Fuzzy Sets Syst., 2016)

An Algebraic Approach to Automatic Reasoning for NetKAT Based on Its Operational Semantics. - Yuxin Deng 001; Min Zhang 002; Guoqing Lei (ICFEM, 2017)

On Equivalence Checking of Nondeterministic Finite Automata. - Chen Fu; Yuxin Deng 001; David N. Jansen; Lijun Zhang 001 (SETTA, 2017)

Bisimulations for probabilistic linear lambda calculi. - Yuxin Deng 001; Yuan Feng 001 (TASE, 2017)

Probabilistic bisimilarity as testing equivalence. - Yuxin Deng 001; Yuan Feng 001 (Inf. Comput., 2017)

Bisimulations for Probabilistic and Quantum Processes (Invited Paper). - Yuxin Deng 001 (CONCUR, 2018)

Generating Permission-Based Security Policies. - Xin Li 010; Hua Vy Le Thanh; Yuxin Deng 001; Julian Dolby (DSA, 2018)

Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems. - Hengyang Wu; Yixiang Chen 001; Tian-Ming Bu; Yuxin Deng 001 (Fuzzy Sets Syst., 2018)

Preface for the special issue of the 10th International Symposium on Theoretical Aspects of Software Engineering (TASE 2016). - Marcello M. Bonsangue; Yuxin Deng 001 (Sci. Comput. Program., 2018)

Distribution-Based Behavioral Distance for Nondeterministic Fuzzy Transition Systems. - Hengyang Wu; Yuxin Deng 001 (IEEE Trans. Fuzzy Syst., 2018)

Formalisation of Probabilistic Testing Semantics in Coq. - Yuxin Deng 001; Jean-François Monin (The Art of Modelling Computational Systems, 2019)

Simulations for Multi-Agent Systems with Imperfect Information. - Patrick Gardy; Yuxin Deng 001 (ICFEM, 2019)

Qsimulation V2.0: An Optimized Quantum Simulator. - Hua Wu; Yuxin Deng 001; Ming Xu 010; Wenjie Du 001 (ICTAC, 2020)

Verifying Quantum Communication Protocols with Ground Bisimulation. - Xudong Qin; Yuxin Deng 001; Wenjie Du 001 (TACAS (2), 2020)

SMT-based generation of symbolic automata. - Xudong Qin; Simon Bliudze; Eric Madelaine; Zechen Hou; Yuxin Deng 001; Min Zhang 002 (Acta Informatica, 2020)

Time-bounded termination analysis for probabilistic programs with delays. - Ming Xu 010; Yuxin Deng 001 (Inf. Comput., 2020)

Reachability of Patterned Conditional Pushdown Systems. - Xin Li 010; Patrick Gardy; Yuxin Deng 001; Hiroyuki Seki (J. Comput. Sci. Technol., 2020)

Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. - Peixin Wang; Hongfei Fu 001; Krishnendu Chatterjee; Yuxin Deng 001; Ming Xu 010 (Proc. ACM Program. Lang., 2020)

Explaining GBDT by Probabilistic Finite-State Automata. - Yinkai Chen; Rui Zhang 115; Xin Qiu; Xin Li 010; Yuxin Deng 001 (ICCPR, 2021)

Learning Attention-Based Translational Knowledge Graph Embedding via Nonlinear Dynamic Mapping. - Zhihao Wang; Honggang Xu; Xin Li 010; Yuxin Deng 001 (PAKDD (3), 2021)

Trustworthiness Derivation Tree: A Model of Evidence-Based Software Trustworthiness. - Yuxin Deng 001; Zezhong Chen; Wenjie Du 001; Bifei Mao; Zhizhang Liang; Qiushi Lin; Jinghui Li (QRS Companion, 2021)

Symbolic Reasoning About Quantum Circuits in Coq. - Wenjun Shi; Qinxiang Cao; Yuxin Deng 001; Hanru Jiang; Yuan Feng 001 (J. Comput. Sci. Technol., 2021)

An optimal quantum error-correcting procedure using quantifier elimination. - Ying-Ji Sun; Ming Xu 010; Yuxin Deng 001 (Quantum Inf. Process., 2021)

Quingo: A Programming Framework for Heterogeneous Quantum-Classical Computing with NISQ Features. - Xiang Fu 003; Jintao Yu; Xing Su; Hanru Jiang; Hua Wu; Fucheng Cheng; Xi Deng; Jinrong Zhang; Lei Jin; Yihang Yang; Le Xu; Chunchao Hu; et al. (ACM Trans. Quantum Comput., 2021)

Encodability Criteria for Quantum Based Systems. - Anna Schmitt 002; Kirstin Peters; Yuxin Deng 001 (FORTE, 2022)

Encodability Criteria for Quantum Based Systems (Technical Report). - Anna Schmitt 002; Kirstin Peters; Yuxin Deng 001 (CoRR, 2022)

Formal semantics of a classical-quantum language. - Yuxin Deng 001; Yuan Feng 001 (Theor. Comput. Sci., 2022)

Model checking QCTL plus on quantum Markov chains. - Ming Xu 010; Jianling Fu; Jingyi Mei; Yuxin Deng 001 (Theor. Comput. Sci., 2022)

An algebraic method to fidelity-based model checking over quantum Markov chains. - Ming Xu 010; Jianling Fu; Jingyi Mei; Yuxin Deng 001 (Theor. Comput. Sci., 2022)

A Sample-Driven Solving Procedure for the Repeated Reachability of Quantum CTMCs. - Hui Jiang 009; Jianling Fu; Ming Xu 010; Yuxin Deng 001; Zhi-Bin Li 005 (CoRR, 2023)

A Sample-Driven Solving Procedure for the Repeated Reachability of Quantum Continuous-time Markov Chains. - Hui Jiang 009; Jianling Fu; Ming Xu 010; Yuxin Deng 001; Zhi-Bin Li 005 (HSCC, 2024)

Local Reasoning About Probabilistic Behaviour for Classical-Quantum Programs. - Yuxin Deng 001; Huiling Wu; Ming Xu 010 (VMCAI (2), 2024)

Algorithmic Analysis of Termination Problems for Nondeterministic Quantum Programs. - Jianling Fu; Hui Jiang 009; Ming Xu 010; Yuxin Deng 001; Zhi-Bin Li 005 (CoRR, 2024)

Qubit Mapping Based on Tabu Search. - Hui Jiang 009; Yuxin Deng 001; Ming Xu 010 (J. Comput. Sci. Technol., 2024)

Formalizing the Semantics of a Classical-Quantum Imperative Language in Coq. - Wenjun Shi; Qinxiang Cao; Yuxin Deng 001 (J. Circuits Syst. Comput., 2024)

A Pattern Matching Based Framework for Quantum Circuit Rewriting. - Hui Jiang 009; Dian-Kang Li; Yuxin Deng 001; Ming Xu 010 (J. Comput. Sci. Technol., 2024)

Termination and Universal Termination Problems for Nondeterministic Quantum Programs. - Ming Xu 010; Jianling Fu; Hui Jiang 009; Yuxin Deng 001; Zhi-Bin Li 005 (ACM Trans. Softw. Eng. Methodol., 2024)

Cycle-Aware Parallel Optimization for Mitigating ZZ Crosstalk on Quantum Hardware. - Jiayi Zhong; Yuxin Deng 001 (ICPP, 2025)

Enhancing Large-Scale Code Understanding Through Goal Structuring Notation and Large Language Models. - Zezhong Chen; Yuxin Deng 001; Wenjie Du 001 (Comput. Informatics, 2025)

Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains. - Ming Xu 010; Jingyi Mei; Ji Guan 001; Yuxin Deng 001; Nengkun Yu (Log. Methods Comput. Sci., 2025)

Trusta: Reasoning about assurance cases with formal methods and large language models. - Zezhong Chen; Yuxin Deng 001; Wenjie Du 001 (Sci. Comput. Program., 2025)

MoDA: Mixture of Domain Adapters for Parameter-efficient Generalizable Person Re-identification. - Yang Wang 019; Yixing Zhang; Xudie Ren; Yuxin Deng 001 (ACM Trans. Multim. Comput. Commun. Appl., 2025)

EZCache: A Hierarchical Memory System for Zoned Neutral Atom Quantum Computers. - Jiayi Zhong; Yuxin Deng 001; Hui Jiang; Jiacheng Feng (ICS, 2026)

DMapS: End-to-End Qubit Mapping and Routing for Distributed Quantum Computing Architectures. - Tingyu Luo; Yuzhen Zheng; Yuxin Deng 001; Xiang Fu 003 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2026)