651 64353

DONG Jin Song

Deputy Head, Department Of Computer Science

  • Ph.D. (University of Queensland, Australia, 1995)
  • B.InfTech. (Software Engineering, 1st Class Honours, University of Queensland, Australia, 1992)

Dr. Jin-Song Dong is a professor at the School of Computing at the National University of Singapore (NUS) and he joined NUS in 1998. His research is in the areas of formal methods, safety and security systems, probabilistic reasoning, sports analytics, and trusted machine learning. He co-founded the PAT verification system which has attracted thousands of registered users from 1000+ organizations in 150 countries and won the 20-year ICFEM Most Influential System Award in 2018 (with Jun and Yang). He also co-founded “Silas: Trusted Machine Learning” and the Dependable Intelligence company ( He received several best paper awards including the ACM SIGSOFT Distinguished Paper Award for ICSE 2020. Jin Song has been on the editorial board of ACM Transaction on Software Engineering and Methodology, Formal Aspects of Computing, and Innovations in Systems and Software Engineering, A NASA Journal. He has successfully supervised 28 PhD students and many of them have become tenured faculty members in leading universities around the world. He is a Fellow of the Institute of Engineers Australia. In his spare time, he developed Markov Decision Process (MDP) models for tennis strategy analysis in PAT and helped professional players in their pre-match analysis (beating the world's best). Jin Song is also a Grand Slam junior coach and enjoys coaching tennis to his 3 kids who all reached the #1 Singapore/Australia national junior ranking (two of his kids received NCAA Division 1 full scholarships, and his 2nd son Chen Dong played #1 singles for Australia in the Junior Davis Cup World Final and played Australian Open and US Open Junior Grand Slams.


  • time concurrent system, specification, semantic web, formal methods, safety critical systems

  • Software Engineering, Formal Methods, Model Checking, Probabilistic Reasoning, Decision Marking, Trusted AI/LLM

  • Safety and Security Systems, Autonomous Systems, Blockchain, Sport Analytics





  • L. Li, J. Sun, Y. Liu, J.S. Dong, M. Sun, A Formal Specification and Verification Framework for Timed Security Protocols, IEEE Transactions on Software Engineering TSE, accepted in May 2017.
  • G. Bai, J. Ye, J. Sun, Y. Liu, W. Visser, J.S. Dong, Towards Model Checking Android Applications, IEEE Transactions on Software Engineering TSE, accepted in March 2017.
  • T. Wang, J. Sun, Y. Liu, J.S. Dong, X. Li. A Systematic Study on Non-Zenoness Checking for Timed Automata. IEEE Transactions on Software Engineering TSE, 411: 3-18 2015
  • J. S. Dong, Y. Liu, J. Sun. Towards Verification of Computation Orchestration. Formal Aspects of Computing FAC journal, Springer, 264: 729-759 2014
  • S. Lin, E. Andre, Y. Liu, J. Sun, J. S. Dong, Learning Assumptions for Compositional Verification of Timed Systems, IEEE Transactions on Software Engineering TSE, 402: 137-153 2014
  • Y. Li, J. S. Dong, J. Sun, Y. Liu. Model Checking Approach to Automated Planning, Formal Methods in System Design FMSD journal, Springer, 442: 176-202 2014
  • Y. Liu, W. Chen, A. Liu, J. S. Dong. Verifying Linearizability via Optimized Refinement Checking. IEEE Transactions on Software Engineering TSE, 397:1018-1039, 2013.
  • J. Sun, Y. Liu, J. S. Dong, E. Andre. Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP. ACM Transactions on Software Engineering and Methodology TOSEM, 221:3:13-29, 2013.


  • Best Paper Award at ICECCS (2015)

  • Best Journal Paper Award at Software and Systems Modeling (SSM) journal (2014)

  • Best Paper Award at ICECCS (2012)

  • ACM SIGSOFT Distinguished Paper Award for ICSE (2020)


Formal Methods for Software Engineering
Formal Specification and Design Techniques


In the News

23 April 2021
23 April 2021 - Thirteen research papers by NUS Computing faculty and students were featured in the 30th Web Conference, ...