Research
My research investigates a synergy of statistical, inductive approaches (represented by deep learning) and logical, deductive approaches (represented by constraint solving), and applys them
to solve a broad range of problems at the interface of Programming Language, Verification, Software Engineering and Machine Learning.
Machine Learning for Software Engineering
Neural code generation and API recommendation
Selected papers
- Xiangyu Zhang, Yu Zhou, Guang Yang, Taolue Chen. Syntax-Aware Retrieval Augmented Code Generation. The 2023 Conference on Empirical Methods in Natural Language Processing
(EMNLP, finding), 2023.
- Guang Yang, Yu Zhou, Xiang Chen, Xiangyu Zhang, Yiran Xu, Tingting Han, Taolue Chen. A Syntax-Guided Multi-Task Learning Approach for Turducken-Style Code Generation. Empirical Software Engineering 28:141. 2023.
- Guang Yang, Yu Zhou, Xiang Chen, Xiangyu Zhang, Tingting Han, Taolue Chen. ExploitGen: Template-Augmented Exploit Code Generation Based on CodeBERT. The Journal of Systems and Software 197: 111577, 2023.
- Yu Zhou, Chen Chen, Yongchao Wang, Tingting Han, Taolue Chen. Context-Aware APIs Recommendation Using Tensor Factorization. Science in China 66, 122101, 2023.
- Yongchao Wang, Yu Zhou, Taolue Chen, Jingxuan Zhang, Wenhua Yang, Zhiqiu Huang. Sequence-Aware API Recommendation based on Collaborative Filtering. International Journal of Software Engineering and Knowledge Engineering. 2022.
(Conference version under the title "Hybrid Collaborative Filtering-Based API Recommendation" at QRS 2021.)
- Yu Zhou, Xinying Yang, Taolue Chen, Zhiqiu Huang, Xiaoxing Ma, Harald C. Gall. Boosting API Recommendation with Implicit Feedback. IEEE Trans. Software Eng. 48(6): 2157-2172, 2022.
(BRAID, and demo video)
- Yu Zhou, Haonan Jin, Xinying Yang, Taolue Chen, Krishna Narasimhan, Harald Gall. BRAID: An API Recommender Supporting Implicit User Feedback (Tool demo). ESEC/FSE 2021.
- Yu Zhou, Juanjuan Shen, Xiaoqing Zhang, Wenhua Yang, Tingting Han, Taolue Chen. Automatic Source Code Summarization with Graph Attention Networks. The Journal of Systems and Software 188, 111257, 2022.
- Liyu Fang, Zhiqiu Huang, Yu Zhou, Taolue Chen. Adaptive Code Completion with Meta-learning. Internetware 2021.
- Juanjuan Shen, Yu Zhou, Yongchao Wang, Xiang Chen, Tingting Han and Taolue Chen. Evaluating Code Summarization with Improved Correlation with Human Assessment. The 21st IEEE International Conference on Software Quality, Reliability, and Security (QRS 2021).
Selected papers
- Yu Zhou, Xiaoqing Zhang, Juanjuan Shen, Tingting Han, Taolue Chen, Harald Gall. Adversarial Robustness of Deep Code Comment Generation. ACM Transactions on Software Engineering and Methodology, 31(4):pp 1–30. 2022.
(Tool ACCENT)
- Yu Zhou, Xin Yan, Wenhua Yang, Taolue Chen, Zhiqiu Huang. Augmenting Java method comments generation with context information based on neural networks. The Journal of Systems and Software 156: 328-340, 2019.
- Xiaoqing Zhang, Yu Zhou, Tingting Han, Taolue Chen. Training Deep Code Comment Generation Model via Data Augmentation. Internetware 2021.
Defects Detection of Software artifacts
API providers tend to release incomplete or inconsistent API documentation, which deviates from the actual API implementation. We formally investigate the issue of inconsistency between API code and its documentation for the first time. We provide a novel method---with tool implementation---to automatically detect and repair defects from API documents. The empirical evaluation shows that the approach and the associated tool are able to find confirmed defects of documents for JDK 1.8 APIs and Android 7.0.
Selected papers:
- Yu Zhou, Changzhi Wang, Xin Yan, Taolue Chen, Sebastiano Panichella, Harald Gall. Automatic Detection and Repair Recommendation of Directive Defects in Java API Documentation. IEEE Trans. Software Eng. (The conference version was presented at ICSE'17.)
- Yu Zhou, Xin Yan, Taolue Chen, Sebastiano Panichella, Harald Gall. DRONE: A Tool to Detect and Repair Directive Defects in Java APIs Documentation. ICSE’19. (DRONE, and demo video)
User review analysis
Machine Learning meets Logic and Verification
Neural Symbolic Systems
- Zenan Li, Yunpeng Huang, Zhaoyu Li, Yuan Yao, Jingwei Xu, Taolue Chen, Xiaoxing Ma, Jian Lu. Neuro-symbolic Learning Yielding Logical Constraints. NeurIPS 2023.
- Zenan Li, Zehua Liu, Yuan Yao, Jingwei Xu, Taolue Chen, Xiaoxing Ma, Jian Lu. Learning with Logical Constraints but without Shortcut Satisfaction. ICLR'23.
- Zenan Li, Yuan Yao, Taolue Chen, Jingwei Xu, Chun Cao, Xiaoxing Ma, Jian Lu. Softened Symbol Grounding for Neuro-symbolic Systems. ICLR'23.
Verification of Neural Networks
- Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song, Taolue Chen. Precise Quantitative Analysis of Binarized Neural Networks: A BDD-based Approach. ACM Transactions on Software Engineering and Methodology 32(3): 62:1-62:51, 2023.
(Conference version under the title BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks at CAV'21. )
- Zhe Zhao, Yedi Zhang, Guangke Chen, Fu Song, Taolue Chen, Jiaxiang Liu. CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial Attacks. 29th International Symposium on Static Analysis (SAS'22).
Lecture Notes in Computer Science 13,790, pp. 449-473. 2022.
- Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song, Min Zhang, Taolue Chen, Jun Sun. QVIP: An ILP-based Formal Verification Approach for Quantized
Neural Networks. ASE'22. (Tool: QVIP)
Quality Assurance for Deep learning
- Zenan Li, Maorun Zhang, Jingwei Xu, Yuan Yao, Chun Cao, Taolue Chen, Xiaoxing Ma, Jian Lu. Lightweight Approaches to DNN Regression Error Reduction: An Uncertainty Alignment Perspective. ICSE'23. 2023
- Sen Wang, Zhuheng Sheng, Jingwei Xu, Taolue Chen, Junjun Zhu, Shuhui Zhang, Yuan Yao, Xiaoxing Ma. ADEPT: A Testing Platform for Simulated Autonomous Driving. ASE'22 (Tool Demo).
Control and ML
- Hengjun Zhao, Xia Zeng, Taolue Chen, Zhimin Liu, Jim Woodcock. Learning Safe Neural Network Controllers with Barrier Certificates. Formal Aspects Comput. 33(3): 437-455, 2021. (Conference version at SETTA'20)
- Hengjun Zhao, Xia Zeng, Taolue Chen, Zhimin Liu. Synthesizing Barrier Certificates Using Neural Networks. HSCC'20.
Verification of multi-agent systems
- Yedi Zhang, Fu Song, Taolue Chen. Making Agents’ Abilities Explicit. IEEE Access 7(1), 101,804-101,819, 2019.
- Fu Song, Yedi Zhang, Taolue Chen, Yu Tang, Zhiwu Xu. Probabilistic Alternating-Time mu-Calculus. AAAI’19, pp. 6179-6186. 2019.
- Taolue Chen, Fu Song, and Zhilin Wu. Model Checking Pushdown Epistemic Game Structures. 19th International Conference on Formal Engineering Methods (ICFEM'17). LNCS 10,610, pp. 36-53, 2017
- Taolue Chen, Fu Song, and Zhilin Wu. Verifying Pushdown Multi-Agent Systems against Strategy Logics. IJCAI’16, pp. 180-186, AAAI Press, 2016.
- Taolue Chen, Fu Song, and Zhilin Wu. Global Model Checking on Pushdown Multi-Agent Systems. AAAI’16, pp. 2459-2465, AAAI Press, 2016.
Software security
Side-channel attacks
Cryptographic algorithms are widely used to protect data privacy in many aspects of daily lives from smart card to cyber-physical systems.
Unfortunately, programs implementing cryptographic algorithms may be vulnerable to practical power side-channel attacks,
which may infer private data via statistical analysis of the correlation between power consumptions of an electronic device and private data.
To thwart these attacks, several masking schemes have been proposed, giving rise to effective countermeasures for reducing the statistical correlation between private data and power consumptions. However, programs that rely on secure masking schemes are not secure a priori. Indeed, designing effective masking programs is a labor intensive and error-prone task. We propose approaches for formally verifying masking countermeasures of cryptographic programs.
Selected papers:
- Pengfei Gao, Yedi Zhang, Fu Song, Taolue Chen, Francois-Xavier Standaert. Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks. Object-Oriented Programming, Systems, Languages & Applications 2023 (OOPSLA 2023). To appear.
(Tool: CONVINCE)
- Pengfei Gao, Fu Song, Taolue Chen. Compositional Verification of First-Order Masking Countermeasures against Power Side-Channel Attacks. ACM Transactions on Software Engineering and Methodology. To appear.
- Mingyang Liu, Fu Song, Taolue Chen. Automated Verification of Correctness for Masked Arithmetic Programs. CAV'23. 2023.
(Tool: FISCHER)
- Qi Qin, JulianAndres JiYang, Fu Song, Taolue Chen, Xinyu Xing. DeJITLeak: Eliminating JIT-Induced Timing Side-Channel Leaks. ESEC/FSE 2022.
- Pengfei Gao, Hongyi Xie, Pu Sun, Jun Zhang, Fu Song, Taolue Chen. Formal Verification of Masking Countermeasures for Arithmetic Programs. IEEE Trans. on Software Eng. 48(3): 973-1000, 2022. (Conference version:
Pengfei Gao, Hongyi Xie, Jun Zhang, Fu Song, Taolue Chen. Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks, at TACAS'19, Tool: QMVerif)
- Pengfei Gao, Hongyi Xie, Fu Song and Taolue Chen. A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs. ACM Trans. Softw. Eng. Methodol. 30(3): 26:1-26:42, 2021.
Secure Multi-Party Computation
Android Multitasking Mechanism
We propose formal models to capture key mechanisms of Android multi-tasking, focusing on the evolution of the back stack of the Android system when interacting with activities.
- Jinlong He, Taolue Chen, Ping Wang, Zhilin Wu, Jun Yan. Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps. APLAS’19, 2019.
- Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu, and Jun Yan. Android Stack Machine. 30th International Conference on Computer Aided Verification (CAV'18). LNCS 10,982, 487-504, 2018.
Program analysis and constraint solving
String constraint solving
String constraint solving is important in a wide range of areas, e.g., program analysis and web security. Previous studies either provide rather fragmented theoretical results on its decidability/complexity, or practical algorithms without completeness guarantees. We identify novel semantical---as opposed to previously syntactic---conditions for string constraints which entail decidability, providing effective decision procedures with detailed complexity analysis, and importantly, efficient implementation as a new string solver Ostrich. The experiments demonstrate the efficacy of the new solver against other competitive solvers. In contrast to previous work, the solver achieves efficiency but without sacrificing theoretical guarantees.
Selected papers:
- Taolue Chen, Matthew Hague, Zhilei Han, Denghang Hu, Alejandro Flores Lamas, Anthony Widjaja Lin, Shuanglong Kan, Philipp Ruemmer, Zhilin Wu. Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables. POPL'22.
- Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Ruemmer, Zhilin Wu. A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. ATVA 2020.
- Taolue Chen, Matthew Hague, Anthony Lin, Philipp Ruemmer, Zhilin Wu. Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations. POPL'19. PACMPL 3(POPL): 49:1-49:30, 2019.
- Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, Zhilin Wu. What Is Decidable about String Constraints with the ReplaceAll Function. Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. 2018.
Tools: Ostrich
Separation logic
- Chong Gao, Taolue Chen, Zhilin Wu. Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints. 45th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), LNCS 11,376, 206-220, Springer, 2019.
- Taolue Chen, Fu Song, and Zhilin Wu. Tractability of Separation Logic with Inductive Definitions: Beyond Lists. 28th International Conference on Concurrency Theory (CONCUR'17), LIPIcs 85, 37:1-37:17, 2017.
- Zhaowei Xu, Taolue Chen, Zhilin Wu. Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. The 26th International Conference on Automated Deduction (CADE-26). LNCS 10395, pp. 509-527, 2017.
- Xincai Gu, Taolue Chen, and Zhilin Wu. A complete decision procedure for linearly compositional separation logic with data constraints. IJCAR’16, LNCS 9706, pp. 532-549, 2016.
Probabilistic verification
Verification of stochastic games
We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal.
Selected papers:
- Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems. Formal Methods in System Design 43(1):61-92, Springer. 2013. (The conference version was presented at TACAS'12.)
- Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, Clemens Wiltsche. On Stochastic Games with Multiple Objectives. MFCS 2013, LNCS 8087, pp. 266-277, Springer, 2013.
- Taolue Chen, Marta Z. Kwiatkowska, Aistis Simaitis, Clemens Wiltsche. Synthesis for Multi-objective Stochastic Games: An Application to Autonomous Urban Driving. QEST 2013, LNCS 8054, pp. 322-337, Springer, 2013.
- Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis. PRISM-games: A Model Checker for Stochastic Multi-Player Games. TACAS 2013, LNCS 7795, pp. 185-191, Springer, 2013.
- Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, Ashutosh Trivedi, Michael Ummels. Playing Stochastic Games Precisely. CONCUR'12, LNCS 7454, pp. 348-363, Springer, 2012.
- Taolue Chen, Marta Kwiatkowska, David Parker and Aistis Simaitis. Verifying Team Formation Protocols with Probabilistic Model Checking. CLIMA XII, LNCS 6814, pp. 190-207, Springer, 2011.
Verification of continuous-time Markov models
We study the verification of finite continuous-time Markov chain against various linear real-time specification including timed automaton, metric temporal logics, linear duratioinal properties. On a more practical side, we carry out quantitative verification of implantable cardiac pacemakers.
Selected papers:
- Taolue Chen, Marco Diciolla, Marta Z. Kwiatkowska, and Alexandru Mereacre. Verification of linear duration properties over continuous-time Markov chains. ACM Transaction on Computational Logic 14(4): 33, 2013. (The conference version was presented at HSCC'12.)
- Taolue Chen, Marco Diciolla, Marta Z. Kwiatkowska, Alexandru Mereacre. Quantitative Verification of Implantable Cardiac Pacemakers over Hybrid Heart Models. Information and Computation 236: 87-101, 2014. (The conference versions were presented at HSCC'13 and RTSS'12.)
- Taolue Chen, Marco Diciolla, Marta Kwiatkowska and Alexandru Mereacre. Time-Bounded Verification of CTMCs Against Real-Time Specifications. FORMATS'11, LNCS 6919, pp. 26-42, Springer, 2011.
- Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. Logical Methods in Computer Science, 7(1-2):1-34, 2011. (The conference version was presented at LICS'09.)
- Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Observing Continuous-Time MDPs by 1-Clock Timed Automata. RP'11, LNCS 6945, pp. 2-25, Spriner, 2011.
- Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Reachability Probabilities in Markovian Timed Automata. CDC'11, pp. 7075-7080, IEEE Press, 2011.
- Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. LTL Model Checking of Time-Inhomogeneous Markov Chains. ATVA'09, LNCS 5799, pp. 104-119, Springer, 2009.
Perturbation analysis and robust verification
We identify discrepancies between a stochastic model used in probabilistic verification and the real-world system it represents when the model is built from statistical data. The issue, which is was overlooked for many years, is that a tiny but nontrivial change to model quantities may lead to misleading or even invalid verification results. We present rigours, mathematical formulation of the problem, with important steps towards a systematic solution. Empirical studies show that the novel notion of asymptotic perturbation bounds can accurately estimate maximum variations of verification results induced by model perturbations.
Selected papers
- Guoxin Su, Yuan Feng, Taolue Chen, and David S. Rosenblum. Perturbation Analysis of Stochastic Systems with Empirical Distribution Parameters: An Asymptotic Approach. IEEE Trans. Software Eng. 42(7): 623-639, 2016.
- Guoxin Su, Taolue Chen, Yuan Feng, and David S. Rosenblum. ProEva: Runtime Proactive Performance Evaluation Based on Continuous-Time Markov Chains. ICSE'17, 2017, IEEE/ACM.
- Guoxin Su, Taolue Chen, Yuan Feng, David S. Rosenblum, and P. S. Thiagarajan. An Iterative Decision-Making Scheme for Markov Decision Processes and Its Application to Self-Adaptive Systems. FASE’16. LNCS 9633 pp. 269-286, 2016.
- Taolue Chen, Yuan Feng, David Rosenblum, Guoxin Su. Perturbation Analysis in Verification of Discrete-Time Markov Chains. CONCUR’14, LNCS 8704, pp. 218-233, 2014.
- Taolue Chen, Tingting Han, Marta Z. Kwiatkowska. On the complexity of model checking interval-valued discrete time Markov chains. Information Processing Letters 113(7): 210-216, 2013.
Verification of Markov Decision Processes
Selected papers:
- Taolue Chen, Stefan Kiefer. On the Total Variation Distance of Labelled Markov Chains. LICS'14, 33:1-33:10, ACM, 2014.
- Tomas Brazdil, Taolue Chen, Vojtech Forejt, Petr Novotny, Aistis Simaitis. Solvency Markov Decision Processes with Interest. FSTTCS'13, LIPIcs volume 24, pages 487-499, 2013.
-
Taolue Chen, Klaus Dräger, Stefan Kiefer. Model Checking Stochastic Branching Processes. MFCS'12, LNCS 7464, pp. 271-282, Springer, 2012.
- Taolue Chen, Tingting Han. On the Complexity of Computing Maximum Entropy for Markovian Models. FSTTCS'14, LIPIcs volume 29, pp. 571-583, 2014.
- Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Kwiatkowska, Hongyang Qu, Lijun Zhang. Model Repair for Markov Decision Processes. TASE'13, pp. 85-92, IEEE Press, 2013.
Axiomatisation of process algebra
Semantics in the linear time–branching time spectrum
Van Glabbeek presented the linear time–branching time spectrum of behavioural semantics. He studied these semantics in the setting of the basic process algebra BCCSP, and gave finite, sound and ground-complete, axiomatisations for most of these semantics. Groote proved for some of van Glabbeek’s axiomatisations that they are ω-complete, meaning that an equation can be derived if (and only if) all of its closed instantiations can be derived. We settle the remaining open questions for all the semantics in the linear time–branching time spectrum, either positively by giving a finite sound and ground-complete axiomatisation that is ω-complete, or negatively by proving that such a finite basis for the equational theory does not exist.
Selected papers:
- Taolue Chen and Wan Fokkink. The Saga of Finite Equational Bases over BCCSP. NVTI (Dutch Association for Theoretical Computer Science) Newsletter, 2010 (Invited contribution).
- Taolue Chen, Wan Fokkink, Rob J. van Glabbeek. On the Axiomatizability of Impossible Futures. Logical Methods in Computer Science, 11(3:17): 1-30, 2015.
- Taolue Chen, Wan Fokkink and Rob van Glabbeek. Ready to Preorder: The Case of Weak Process Semantics. Information Processing Letters 109(2): 104-111, Elsevier, 2008.
- Taolue Chen, Wan Fokkink, Bas Luttik and Sumit Nain. On Finite Alphabets and Infinite Bases. Information and Computation 206(5): 492-519, Elsevier, 2008.
Priority operator
- Luca Aceto, Taolue Chen, Anna Ingolfsdottir, Bas Luttik and Jaco van de Pol. On the Axiomatizability of Priority II. TCS. 412(28): 3035-3044, 2011.
- Luca Aceto, Taolue Chen, Wan Fokkink and Anna Ingolfsdottir. On the Axiomatizability of Priority. Mathematical Structure in Computer Science 18(1): 5-28, Cambridge University Press, 2008. (Conference version appeared in ICALP'06).
Prefix iteration
- Taolue Chen and Jian Lu. Complete Axiomatization for Divergent-sensitive Bisimulations in Basic Process Algebra with Prefix Iteration. The First International Conference on Foundations of Informatics, Computing and Software (FICS'08). ENTCS 212: 55-70. Elsevier.
- Taolue Chen, Tingting Han and Jian Lu. On the Complete Axiomatization for Prefix Iteration modulo Observation Congruence. Acta Cybernetica: 17(3), 2006.