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)

Jin Song has joined in the School of Computing at the National University of Singapore (NUS) in 1998 and currently he is a full professor at SoC. His research is in the areas of formal methods, model checking, semantic technology, safety & security critical systems and probabilistic reasoning. With his former PhD student Sun Jun and Liu Yang, they co-founded PAT reasoning system which has attracted 4000+ registered users from 900+ organizations in 89 countries, including, e.g., AutoNetworks Tech, Toyota, NTT, Mitsubishi, Japan Aerospace eXploration Agency, BD Biosciences, etc. Jin Song is 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. Jin Song has been a Visiting Fellow at Oxford University, UK, and a Visiting Professor at National Institute of Informatics, Japan. He has successfully supervised 25 PhD students and many of them have become tenure track faculty members in the leading universities around the world, including NTU, SUTD, HUST, Tianjin U, Monash U and Auckland U.


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

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

  • 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)

  • IEEE Reliability Society Leadership Award In Recognition of Outstanding Leadership and Services as the General Chair of the 4th IEEE International Conference on Secure Software & Reliability Improvement (SSIRI), 2010.


Formal Methods for Software Engineering
Formal Specification and Design Techniques