Intensionality of modal logic for Robust Ambient Calculus. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (FGC, 2003)

Framework of Performance Evaluation for Mobile Process Based on Mobile Ambient. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (CIT, 2004)

Towards a Model Logic for p-Calculus. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (COMPSAC, 2004)

Tree logic with recursion and model checking algorithm. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (IASTED Conf. on Software Engineering and Applications, 2004)

A Modal Logic for pi-Calculus and Model Checking Algorithm. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (WoLLIC, 2004)

Checking Strong Open Congruence in Chi -Calculus. - Taolue Chen 001; Jingyang Zhou; Tingting Han 001; Jian Lu 001 (CATS, 2004)

Analysis of A Leader Election Algorithm in uCRL. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (CIT, 2005)

Structure Analysis for Dynamic Software Architecture Based on Spatial Logic. - Tingting Han 001; Taolue Chen 001; Jian Lu 001 (COMPSAC (1), 2005)

On the Bisimulation Congruence in chi-Calculus. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (FSTTCS, 2005)

Structure Analysis for Dynamic Software Architecture. - Tingting Han 001; Taolue Chen 001; Jian Lu 001 (SNPD, 2005)

On the Markovian Randomized Strategy of Controller for Markov Decision Processes. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (FSKD, 2006)

On the Complete Axiomatization for Prefix Iteration modulo Observation Congruence. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (Acta Cybern., 2006)

Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking. - Tingting Han 001; Joost-Pieter Katoen (ATVA, 2007)

07101 Working Group Report – Performance Measures Other Than Time. - Lucia Cloth; Pepijn Crouzen; Matthias Fruth; Tingting Han 001; David N. Jansen; Mark Kattenbelt; Gerard J. M. Smit; Lijun Zhang 001 (Quantitative Aspects of Embedded Systems, 2007)

On Behavioral Metric for Probabilistic Systems: Definition and Approximation Algorithm. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (FSKD (2), 2007)

Counterexamples in Probabilistic Model Checking. - Tingting Han 001; Joost-Pieter Katoen (TACAS, 2007)

Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains. - Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (HSCC, 2008)

Regular Expressions for PCTL Counterexamples. - Berteun Damman; Tingting Han 001; Joost-Pieter Katoen (QEST, 2008)

Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability. - Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (RTSS, 2008)

Time-Abstracting Bisimulation for Probabilistic Timed Automata. - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen (TASE, 2008)

LTL Model Checking of Time-Inhomogeneous Markov Chains. - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (ATVA, 2009)

Diagnosis, Synthesis and Analysis of Probabilistic Models. - Tingting Han 001 (Ausgezeichnete Informatikdissertationen, 2009)

Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (LICS, 2009)

On metrics for probabilistic systems: Definitions and algorithms. - Taolue Chen 001; Tingting Han 001; Jian Lu 001 (Comput. Math. Appl., 2009)

Counterexample Generation in Probabilistic Model Checking. - Tingting Han 001; Joost-Pieter Katoen; Berteun Damman (IEEE Trans. Software Eng., 2009)

Diagnosis, synthesis and analysis of probabilistic models. - Tingting Han 001 (2009)

Learning-Based Compositional Verification for Synchronous Probabilistic Systems. - Lu Feng 001; Tingting Han 001; Marta Z. Kwiatkowska; David Parker 001 (ATVA, 2011)

Reachability probabilities in Markovian Timed Automata. - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (CDC/ECC, 2011)

Synthesis for PCTL in Parametric Markov Decision Processes. - Ernst Moritz Hahn; Tingting Han 001; Lijun Zhang 001 (NASA Formal Methods, 2011)

Observing Continuous-Time MDPs by 1-Clock Timed Automata. - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (RP, 2011)

Efficient CTMC Model Checking of Linear Real-Time Objectives. - Benoît Barbot; Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (TACAS, 2011)

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (Log. Methods Comput. Sci., 2011)

Quantitative Timed Analysis of Interactive Markov Chains. - Dennis Guck; Tingting Han 001; Joost-Pieter Katoen; Martin R. Neuhäußer (NASA Formal Methods, 2012)

Automatic energy-aware performance analysis of Mobile Ad-Hoc Networks. - Lucia Gallina; Tingting Han 001; Marta Z. Kwiatkowska; Andrea Marin; Sabina Rossi; Alvise Spanò (Wireless Days, 2012)

A process algebraic framework for estimating the energy consumption in ad-hoc wireless sensor networks. - Lucia Gallina; Andrea Marin; Sabina Rossi; Tingting Han 001; Marta Z. Kwiatkowska (MSWiM, 2013)

Model Repair for Markov Decision Processes. - Taolue Chen 001; Ernst Moritz Hahn; Tingting Han 001; Marta Z. Kwiatkowska; Hongyang Qu 001; Lijun Zhang 001 (TASE, 2013)

Modal Specifications for Probabilistic Timed Systems. - Tingting Han 001; Christian Krause 001; Marta Z. Kwiatkowska; Holger Giese (QAPL, 2013)

On the complexity of model checking interval-valued discrete time Markov chains. - Taolue Chen 001; Tingting Han 001; Marta Z. Kwiatkowska (Inf. Process. Lett., 2013)

On the Complexity of Computing Maximum Entropy for Markovian Models. - Taolue Chen 001; Tingting Han 001 (FSTTCS, 2014)

Continuous-time orbit problems are decidable in polynomial-time. - Taolue Chen 001; Nengkun Yu; Tingting Han 001 (Inf. Process. Lett., 2015)

Model based analysis of insider threats. - Taolue Chen 001; Tingting Han 001; Florian Kammueller; Ibrahim Nemli; Christian W. Probst (Cyber Security And Protection Of Digital Services, 2016)

Probabilistic verification of hierarchical leader election protocol in dynamic systems. - Yu Zhou 010; Nvqi Zhou; Tingting Han 001; Jiayi Gu; Weigang Wu (Frontiers Comput. Sci., 2018)

Personal verification based on multi-spectral finger texture lighting images. - Raid Rafi Omar Al-Nima; Musab T. S. Al-Kaltakchi; Saadoon A. M. Al-Sumaidaee; Satnam Singh Dlay; Wai Lok Woo; Tingting Han 001; Jonathon A. Chambers (IET Signal Process., 2018)

Bisimulations for fuzzy transition systems revisited. - Hengyang Wu; Taolue Chen 001; Tingting Han 001; Yixiang Chen 001 (Int. J. Approx. Reason., 2018)

Polynomial-time algorithms for computing distances of fuzzy transition systems. - Taolue Chen 001; Tingting Han 001; Yongzhi Cao (Theor. Comput. Sci., 2018)

Road Tracking Using Deep Reinforcement Learning for Self-driving Car Applications. - Raid Rafi Omar Al-Nima; Tingting Han 001; Taolue Chen 001 (CORES, 2019)

Deep finger texture learning for verifying people. - Raid Rafi Omar Al-Nima; Tingting Han 001; Saadoon A. M. Al-Sumaidaee; Taolue Chen 001 (IET Biom., 2019)

Training Deep Code Comment Generation Models via Data Augmentation. - Xiaoqing Zhang; Yu Zhou 010; Tingting Han 001; Taolue Chen 001 (Internetware, 2020)

Finger Texture Biometric Characteristic: a Survey. - Raid Rafi Omar Al-Nima; Tingting Han 001; Taolue Chen 001; Satnam Singh Dlay; Jonathon A. Chambers (CoRR, 2020)

Probabilistic analysis of QoS-aware service composition with explicit environment models. - Yu Zhou 010; Tingting Han 001; Taolue Chen 001; Shiqi Zhou (IET Softw., 2020)

Evaluating Code Summarization with Improved Correlation with Human Assessment. - Juanjuan Shen; Yu Zhou 010; Yongchao Wang; Xiang Chen 005; Tingting Han 001; Taolue Chen 001 (QRS, 2021)

Robustness and performance of Deep Reinforcement Learning. - Raid Rafi Omar Al-Nima; Tingting Han 001; Saadoon A. M. Al-Sumaidaee; Taolue Chen 001; Wai Lok Woo (Appl. Soft Comput., 2021)

Test Reuse based on Adaptive Semantic Matching across Android Mobile Applications. - Shuqi Liu; Yu Zhou 010; Tingting Han 001; Taolue Chen 001 (QRS, 2022)

Automatic source code summarization with graph attention networks. - Yu Zhou 010; Juanjuan Shen; Xiaoqing Zhang; Wenhua Yang 001; Tingting Han 001; Taolue Chen 001 (J. Syst. Softw., 2022)

Adversarial Robustness of Deep Code Comment Generation. - Yu Zhou 010; Xiaoqing Zhang; Juanjuan Shen; Tingting Han 001; Taolue Chen 001; Harald C. Gall (ACM Trans. Softw. Eng. Methodol., 2022)

ExploitGen: Template-augmented exploit code generation based on CodeBERT. - Guang Yang 019; Yu Zhou 010; Xiang Chen 005; Xiangyu Zhang 005; Tingting Han 001; Taolue Chen 001 (J. Syst. Softw., 2023)

Context-aware API recommendation using tensor factorization. - Yu Zhou 010; Chen Chen; Yongchao Wang; Tingting Han 001; Taolue Chen 001 (Sci. China Inf. Sci., 2023)

A syntax-guided multi-task learning approach for Turducken-style code generation. - Guang Yang 019; Yu Zhou 010; Xiang Chen 005; Xiangyu Zhang 005; Yiran Xu; Tingting Han 001; Taolue Chen 001 (Empir. Softw. Eng., 2023)

Context-aware code generation with synchronous bidirectional decoder. - Xiangyu Zhang 005; Yu Zhou 010; Guang Yang 019; Tingting Han 001; Taolue Chen 001 (J. Syst. Softw., 2024)

Enhancing test reuse with GUI events deduplication and adaptive semantic matching. - Shuqi Liu; Yu Zhou 010; Longbing Ji; Tingting Han 001; Taolue Chen 001 (Sci. Comput. Program., 2024)

DRIVE: Dockerfile Rule Mining and Violation Detection. - Yu Zhou 010; Weilin Zhan; Zi Li; Tingting Han 001; Taolue Chen 001; Harald C. Gall (ACM Trans. Softw. Eng. Methodol., 2024)

Assessing and improving syntactic adversarial robustness of pre-trained models for code translation. - Guang Yang 019; Yu Zhou 010; Xiangyu Zhang 005; Xiang Chen 005; Tingting Han 001; Taolue Chen 001 (Inf. Softw. Technol., 2025)

Integrating behavioral semantic analysis in usage-based equivalent tests generation for mobile applications. - Shuqi Liu; Yu Zhou 010; Huiwen Yang; Tingting Han 001; Taolue Chen 001 (Sci. Comput. Program., 2025)