Taolue Chen

 

School of Computing and Mathematical Sciences, Faculty of Science, Birkbeck, University of London, United Kingdom

Office: MAL158

Email: t.chen#bbk.ac.uk; taolue.chen#gmail.com [@/#]

Postal address: School of Computing and Mathematical Sciences, Birkbeck, University of London, Malet Street, London WC1E 7HX, United Kingdom

University Official Profile

 

I am a computer scientist and an applied mathematician working in

  • Software Engineering, Program Analysis and Verification
  • Machine Learning, Probabilistic Modelling

I am particularly interested in the interactions of these subjects. I also have general interests in (both continuous and discrete) Mathematics broadly related to Computer Science (e.g., Algorithms, Computational Complexity and Quantum Computing).

Please check here for a brief summary of my research, and here or DBLP, Google Scholar for publications.

Research

My research interest lies in neuro-symbolic software engineering, which is to investigate a synergy of statistical (aka data-driven), inductive approaches (represented by deep learning) and logical, deductive approaches (represented by constraint solving), and to apply them to solve a broad range of problems at the interface of Software Engineering, Programming Language and Verification.

Neuro-symbolic Software Enginnering and Verificaton

Neural Code Generation

Selected papers

Deep Learning for Verification

  • Guangyuan Wu, Weining Cao, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma. LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference. ASE'24. (ACM SIGSOFT Distinguished Paper Award)
  • Jiahe Xu, Jingwei Xu, Taolue Chen, Xiaoxing Ma. Symbolic Execution with Test Cases Generated by Large Language Models. QRS'24, IEEE, 2024
  • 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.

Neural Comments Generation

Neuro-Symbolic Learning

Quality Assurance for Deep learning

Machine Learning for Software Evolution

  • 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)
  • Yu Zhou, Yanqi Su, Taolue Chen, Zhiqiu Huang, Harald Gall, Sebastiano Panichella. User Review-Based Change File Localization for Mobile Applications. IEEE Trans. Software Eng. 47(12):2755-2770, 2021.

Program Analysis and Constraint Solving

Program Verification for 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:

Model Based Analysis and Testing (Mainly for Android)

  • Shuqi Liu, Yu Zhou, Longbing Ji, Tingting Han, Taolue Chen. Enhancing test reuse with GUI events deduplication and adaptive semantic matching. Science of Computer Programming, 232(2024), 103052.
  • Shuqi Liu, Yu Zhou, Tingting Han, Taolue Chen. Test Reuse Based on Adaptive Semantic Matching across Android Mobile Applications. 22nd IEEE International Conference on Software Quality, Reliability, and Security (QRS'22). IEEE. 2022.
  • Pengfei Gao, Yongjie Xu, Fu Song, Taolue Chen. Model-based automated testing of JavaScript Web applications via longer test sequences. Frontiers Comput. Sci. 16(3): 163204, 2022.
  • 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.

Secure Multi-Party Computation

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:

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.

Selected Publication

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2005-2010

Book


Teaching

  • Systems Analysis and Design
  • Analytic Tools for Data Science

    •  

    All teaching materials are available at Moodle

    Office Hours: by appointment