National University of Singapore

Dr. DONG, Jin Song Professor, Computer Science Department, School of Computing, National University of Singapore 13 Computing Drive Singapore 117417 E-mail: dcsdjs at nus dot edu dot sg or dongjs1@gmail.com (currently on sabbatical leave)

Brief Bio

• Dr. Jin-Song Dong is a full professor at the National University of Singapore. His research spans a range of fields, including formal methods, safety and security systems, probabilistic reasoning, sports analytics, trusted machine learning, and verified LLM code synthesis. He co-founded the commercialized PAT verification system, which has garnered thousands of registered users from over 150 countries. Jin Song co-founded the commercialized trusted machine learning system Silas (www.depintel.com). He served on the editorial board of ACM Transactions on Software Engineering and Methodology, Formal Aspects of Computing, and Innovations in Systems and Software Engineering, A NASA Journal. He has successfully supervised 33 PhD students, many of whom have become tenured faculty members at leading universities worldwide. He is also a Fellow of the Institute of Engineers Australia. Jin Song developed Markov Decision Process (MDP) models for tennis strategy analysis using PAT, assisting professional players with pre-match analysis (outperforming the world's best). In his spare time, he is a Junior Grand Slam coach and takes pleasure in coaching tennis to his students, and his three children, all of whom have reached the #1 national junior ranking in Singapore/Australia. Two of his children have earned NCAA Division 1 full scholarships, while his second son, Chen Dong (professionally ranked in ATP), played #1 singles for Australia in the Junior Davis Cup World Final and participated in both the Australian Open and US Open Junior Grand Slams.

Research areas

• design analysis and model checking (PAT)
• trusted machine learning, LLM, and decision making (Silas)
• sports analytics (new ISACE series)
• context awareness and pervasive computing (Semantic Space)
• real-time concurrent system specification (TCOZ)
• ontology, services, agent and reasoning
• formal methods and safety/security critical systems
• object, component, and language semantics

Qualifications

• PhD, University of Queensland, Australia (93 - 95) 

• BInfTech with First Class Honours, University of Queensland, Australia (89-92) - Major in Software Engineering.
  

Work Experiences

• Professor (2016) Associate Professor (2005) Assistant Professor (1998),
  Computer Science Department , School of Computing, National University of Singapore (NUS)
  
  • Deputy Head (CS Department, 2023-2024).
  • Faculty Promotion Committee (SoC, 2021-current).
  • Graduate Committee (SoC, 2001-2014, 2022-current).
  • NUS Senate Member (2020-current)
  • Search Committee (CS Department, 2005-2008, 2019-2023).
  • Member of PhD supervisors at NUS Graduate School for Integrative Sciences and Engineering (NGS)
  • Assistant Dean (Graduate Office, SoC, 2005-2008, 2022).
  • SINGA committee Member (NUS, 2007-2009).
  • Co-Director of the IPAL Lab (2013-2019)
  • Publication Ranking Committee (CS Department, 2001-2010).
  • PhD QE Co-ordinator (CS Department, 2008-2014).
  • CS Exco Committee Member (CS Department, 2008-2011).
• Senior Research Scientist (1998),
  Research Scientist (1995-98),
  Division of Mathematical and Information Sciences,
  Commonwealth Scientific and Industrial Research Organisation (CSIRO), Australia
• Tutor (1991-95), CS Department, The University of Queensland.
• Senior Research Assistant, Software Verification Research Centre (11/92-1/93)
  Research Assistant, CS Dept, The University of Queensland (11/91-1/92)

Some Awards/Recognition

• ACM SIGSOFT Distinguished Paper Award for ICSE 2020
• NUS Research Recognition Award (2020)
• Fellow of Institute of Engineers Australia (2018)
• 20 Year ICFEM Most Influential System Award (2018)
• Visiting Fellow at Kellogg College, Oxford University (elected during 2006 sabbatical)
• NUS Young Researcher Award (2004)
• Richard Jago Memorial Prize (1995),
• Australian Postgraduate Award (93-95)

Some Professional and Research Activities

• Organisations:
  • Editorial Board Member of ACM Transactions on Software Engineering and Methodology (ACM TOSEM) (2015-2020)
  • Editorial Board Member of Formal Aspects of Computing Journal (FAoC)
  • Editorial Board Member of Innovations in Systems and Software Engineering, A NASA Journal (ISSE)
  • Advisory Board Member of FME, Formal Methods Europe
  • Steering Committee Member of ICFEM, International Conference on Formal Engineering Methods
  • Steering Committee Member of PRDC, IEEE Pacific Rim International Symposium on Dependable Computing
  • Steering Committee Member of APSEC, Asia-Pacific Software Engineering Conference
  • General Chair of the 19th International Symposium on Formal Methods, FM'14, Singapore, May 2014.
  • General Co-Chair of 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'13), Singapore, July 2013.
  • General Co-Chair of The 15th International Conference on Formal Engineering Methods, Queenstown, NZ. Oct 29 - Nov 1, 2013.
  • Program Co-Chair of The 12th International Conference on Formal Engineering Methods, Shanghai, China, Nov 2010.
  • General Chair of 8th International Symposium on Automated Technology for Verification and Analysis (ATVA'10) 21-24 September 2010, Singapore
  • General Chair of The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI'10), Singapore, 9-11 June, 2010
  • Conference Co-Chair of 6th International Conference on Integrated Formal Methods (IFM'07), Oxford, UK, 2-6 July 2007
  • Program Co-Chair of 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'07), Auckland, NZ, 11-14 July 2007.
  • Tutorial Chair of the 14th International Symposium on Formal Methods, FM 2006, Canada.
  • Program Co-Chair of International Workshop on Web Languages and Formal Methods WLFM 2005, UK.
  • Program Co-Chair of ICFEM 2003, Singapore.
  • Program Co-Chair of APSEC 2000, Singapore.
• Program Committee Member of
  • The 36th International Conference on Software Engineering, ICSE'14, Hyderabad, India, June 1-7, 2014, ICSE'10, Cape Town, May 2010
  • FM 2011: 17th International Symposium of Formal Methods, Ireland. June 2011. FM'09, Eindhoven, the Netherlands, 13th FM'05, Newcastle, UK. FM'99, World Congress, Toulouse France, 1999.
  • 9th International Conference on Integrated Formal Methods IFM2012, Pisa, Italy. IFM2010, Nancy, France. IFM'07, Oxford, UK, IFM'05, Eindhoven, The Netherlands. Nov 2005 , IFM'04, Canterbury UK . IFM'02, Turku, Finland . IFM'00, Schloss Dagstuhl, Germany . IFM'99, York, UK .
  • 13th ICFEM 2011, Durham, UK. 10th ICFEM 2008, Kitakyushu-City, Japan. ICFEM'07, Florida, USA.. ICFEM'05, Manchester UK. ICFEM'04, Seattle USA. ICFEM'03, Singapore. ICFEM'02, Shanghai China, ICFEM'00, York UK , ICFEM'98, Brisbane Australia
  • The 2nd NASA Formal Methods Symposium NFM'10, Washington D.C., April 13-15, 2010
  • The 5th Annual European Semantic Web Conference ESWC 2008, Tenerife, Spain. 2008
  • The 5th International Semantic Web Conference ISWC 2006, Athens, USA. and SWESE 2006
  • 4th International Conference of B and Z Users ZB'05, Guildford UK,
  • 11th IEEE International Conference on Engineering of Complex Computer Systems ICECCS'06, Stanford University, USA. ICECCS'05, Shanghai China. ICECCS'04, Florence, Italy. ICECCS'02, Greenbelt USA. ICECCS'01, Skovde, Sweden . ICECCS'00, Tokyo, Japan. ICECCS'99, Las Vegas, USA.
  • 8th International Conference on Quality Software, QSIC'08, Oxford, UK. QSIC'07, Oregon USA . QSIC'05, Melbourne Australia. QSIC'04 Braunschweig Germany. QSIC'03, Dallas USA. APAQS'01, Hong Kong .
  • 15th APSEC'08, Beijing, China. APSEC'07, Nagoya, Japan. APSEC'06, Bangalore, India. APSEC'04, Busan, Korea. APSEC'03, Chiangmai, Thailand. APSEC'02, Gold Coast, Australia . APSEC'01, Macau . APSEC'00, Singapore . APSEC'99, Takamatsu Japan
  • 5th IEEE International Conference on Software Engineering and Formal Methods SEFM'07, London, UK. SEFM'05, Koblenz Germany. SEFM'04, Beijing China. SEFM'03, Brisbane Australia.
  • 20th International Conference on Software Engineering and Knowledge Engineering, SEKE'08, San Francisco, USA. SEKE'07, Boston, USA. SEKE'06, San Francisco Bay, USA.
  SEKE'05, Taipei Taiwan, 2005
• Research projects

Publications

Book/Editorship

• S. Mirjalili, J. S. Dong, A. Lewis: Nature-Inspired Optimizers - Theories, Literature Reviews and Applications. Springer 2020
• S. Mirjalili, J. S. Dong, Multi-objective optimization using artificial intelligence techniques Springer, 2020
• J. S. Dong and H. Zhu (Editors), Formal Methods and Software Engineering, Proceedings of the 12th International Conference on Formal Engineering Methods, LNCS (vol 2885), Springer-Verlag, Nov 2010.
• J. S. Dong and J. Sun (Editors). Special Issue on the Grand Verification Challenge, Science of Computer Programming, Volume 74(4): (2009)
• A. Arenas, J. S. Dong, A. Martin, B. Matthews (Editors). Special Issue on Web Languages and Formal Methods (WLFM'05). Electr. Notes Theor. Comput. Sci. 151(2): (2006)
• J. S. Dong and J. Woodcock (Editors), Formal Methods and Software Engineering, Proceedings of the 5th International Conference on Formal Engineering Methods, LNCS (vol 2885), Springer-Verlag, Nov 2003.
• J. S. Dong, J. He and M. Purvis (Editors), Proceedings of The 7th Asia-Pacific Software Engineering Conference, IEEE Press. Dec 2000.

Refereed Papers in Journals/Monographs/Conferences (partial list)

• Y Zhang, Y Cai, X Zuo, X Luan, K Wang, M Sun, Z Hou, J Sun, J Dong, Trustworthy AI Agents Require the Integration of LLM with Formal Methods, ICML 2025
• X Weng, J An, X Ma, B Qi, J Luo, X Yang, J Dong, L Huang, Clustering Properties of Self-Supervised Learning, ICML 2025
• Q Zhou, T Li, Q Guo, D Wang, Y Lin, Y Liu, J Dong, Defending LVLMs Against Vision Attacks through Partial-Perception Supervision, ICML 2025
• Y Cai, Z Hou, D Sanan, X Luan, Y Lin, J Sun, J Dong. Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus. POPL, 2025
• Z Liu, J Kun, Z Hou, J Dong, F3Set Towards Analyzing Fast, Frequent, and Fine-grained Events from Videos, ICLR, 2025
• W Jin, Y Cao, J Su, D Wang, Y Zhang, M Xue, J Hao, JS Dong, Y Yang, Whispering Under the Eaves: Protecting User Privacy Against Commercial and LLM-powered Automatic Speech Recognition Systems, Usenix Sec 2025
• Y Zhang, L Huang, P Gao, F Song, J Sun, J Dong, Verification of Bit-Flip Attacks against Quantized Neural Networks, OOPSLA 2025
• Y Zhang, G Chen, F Song, J Sun, JS Dong, Certified Quantization Strategy Synthesis for Neural Networks, International Symposium on Formal Methods (FM), 2024.
• R Liu, Y Lin, X Teoh, Z Huang, J Dong. Less Defined Knowledge and More True Alarms: Reference-based Phishing Detection without a Pre-defined Reference List (USENIX Security 2024).
• X Teoh, Y Lin, R Liu, Z Huang, J Dong. PhishDecloaker: Detecting CAPTCHA-cloaked Phishing Websites via Hybrid Vision-based Interactive Models (USENIX Security 2024).
• C Liu, Y Cai, Y Lin, Y Huang, Y Pei, J Dong, H Mei. CoEdPilot: Recommending Code Edits with Learned Prior Edit Relevance, Project-wise Awareness, and Interactive Nature (ISSTA 2024).
• Y Pan, J Liu, T Zhao, L Zhang, Y Lin, J Dong. A Symbolic Rule Integration Framework with Logic Transformer for Inductive Relation Prediction (WWW 2024).
• J Liu, X Liao, J Dong, A Quaternion-Valued Neural Network Approach to Nonsmooth Nonconvex Constrained Optimization in Quaternion Domain, IEEE Transactions on Emerging Topics in Computational Intelligence, 2023
• J Liu, X Liao, JS Dong, A Recurrent Neural Network Approach for Constrained Distributed Fuzzy Convex Optimization. IEEE Transactions on Neural Networks and Learning Systems. 2023
• Y Cai, Y Lin, C Liu, J Wu, Y Zhang, Y Liu, Y Gong, JS Dong. On-the-Fly Adapting Code Summarization on Trainable Cost-Effective Language Models (NeurIPS 2023).
• Z Liu, K Jiang, Z Hou, Y Lin, JS Dong. Insight Analysis for Tennis Strategy and Tactics (ICDM 2023).
• X Yang, Y Lin, Y Zhang, L Huang, JS Dong, H Mei. An Interactive Time-Travelling Debugging Approach for Deep Classifiers (FSE 2023).
• M Liu, Y Lin, J Liu, B Liu, Q Zheng, JS Dong. B2-Sampling: Fusing Balanced and Biased Sampling for Graph Contrastive Learning (KDD 2023).
• J Wang, M Luo, J Li, Y Lin, JS Dong, Q Zheng. Empower Post-hoc Graph Explanations with Information Bottleneck: A Pre-training and Fine-tuning Perspective (KDD 2023).
• R Liu, Y Lin, Y Zhang, PH Lee, JS Dong. Knowledge Expansion and Counterfactual Interaction for Reference-Based Phishing Detection (USENIX Security 2023).
• X Ren, Y Lin, Y Xue, R Liu, J Sun, Z Feng, JS Dong. DeepArc: Modularizing Neural Networks for the Model Maintenance (ICSE 2023).
• H. Meng, Q. Zhang, G. Xia, Y. Zheng, Y. Zhang, G. Bai, Z. Liu, S. Teo, J. S. Dong Post-GDPR Threat Hunting on Android Phones: Dissecting OS-level Safeguards of User-unresettable Identifiers The Network and Distributed System Security Symposium (NDSS), 2023.
• R. Liu, Y. Lin, X. Yang, J. S. Dong. Debugging and Explaining Metric Learning Approaches: An Influence Function Based Perspective (NeurIPS 2022).
• K. Wang, Y. Zheng, Q. Zhang, G. Bai, M. Qin, D. Zhang, J. S. Dong Assessing Certificate Validation User Interfaces of WPA Supplicants The 28th Annual International Conference On Mobile Computing And Networking (MobiCom), 2022.
• Y. Ling, K. Wang, G. Bai, H. Wang, J. S. Dong Are They Toeing the Line? Diagnosing Privacy Compliance Violations among Browser Extensions The 37th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2022.
• Y. Xiao, Y. Lin, I. Beschastnikh, C. Sun, D. Rosenblum, J. S. Dong. Repairing Failure-inducing Inputs with Input Reflection (ASE 2022).
• S. Li, X. Xie, Y. Lin, Y. Li, R. Feng, X. Li, W. Ge, J. S. Dong. Deep Learning for Coverage-Guided Fuzzing: How Far Are We? (IEEE Trans. Dependable and Secure Computing, TDSC 2022).
• Y. Xiao, I. Beschastnikh, Y. Lin, R. S. Hundal, X. Xie, D. Rosenblum, J. S. Dong. Self-Checking Deep Neural Networks for Anomalies and Adversaries in Deployment (TDSC 2022).
• H. Meng, G. Bai, S. G. Teo, Z. Hou, Y. Xiao, Y. Lin, J. S. Dong. Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective (TDSC 2022).
• X. Song, Y. Lin, S. H. Ng, Y. Wu, X. Peng, J. S. Dong and H. Mei. RegMiner: Towards Constructing a Large Regression Dataset from Code Evolution History (ISSTA 2022).
• X. Yang, Y. Lin, R. Liu, J. S. Dong. Temporality Spatialization: A Scalable and Faithful Time-Travelling Visualization for Deep Classifier Training (IJCAI 2022).
• R. Liu, Y. Lin, X. Yang, S. H. Ng, D. M. Divakaran, and J. S. Dong. Inferring Phishing Intention via Webpage Appearance and Dynamics: A Deep Vision Based Approach (USENIX Security 2022).
• Y. Liang, Y. Lin, X. Song, J. Sun, Z. Feng, J. S. Dong. gDefect4DL: A Dataset of General Real-World Deep Learning Program Defects (ICSE 2022, demo track).
• X. Yang, Y. Lin, R. Liu, Z. He, C. Wang, J. S. Dong, and H. Mei. DeepVisualInsight: Time-Travelling Visualization for Spatio-Temporal Causality of Deep Classification Training (AAAI 2022, Oral Presentation)
• Y. Lin, Y. S. Ong, J. Sun, G. Fraser, J. S. Dong. Graph-based Seed Object Synthesis for Search-Based Unit Testing (ESEC/FSE 2021)
• Y. Lin, R. Liu, D. M. Divakaran, J. Y. Ng, Q. Z. Chan, Y. Lu, Y. Si, F. Zhang, J. S. Dong. Phishpedia: A Hybrid Deep Learning Based Approach to Visually Identify Phishing Webpages (USENIX Security 2021)
• Y. Xiao, I. Beschastnikh, D. S. Rosenblum, C. Sun, S. Elbaum, Y. Lin, J. S. Dong. Self-Checking Deep Neural Networks in Deployment (ICSE 2021)
• Q. Li, Y. Qi, Q. Hu, Y. Lin, J. S. Dong. Adversarial Adaptive Neighborhood with Feature Importance-Aware Convex Interpolation (TIFS 2021)
K. Mahadewa, K. Wang, G. Bai, L. Shi, Y. Liu, J. S. Dong, Z. Liang: Scrutinizing Implementations of Smart Home Integrations. IEEE Trans. Software Eng. 47(12): 2667-2683 (2021)
• H. Bride, J. S. Dong, R. Green, Z. Hóu, B. P. Mahony, M. Oxenham: GRAVITAS: A model checking based planning and goal reasoning framework for autonomous systems. Eng. Appl. Artif. Intell. 97: 104091 (2021)
• H. Bride, C.-H. Cai, J. Dong, J. S. Dong, Z. Hóu, S. Mirjalili, J. Sun: Silas: A high-performance machine learning foundation for logical reasoning and verification. Expert Syst. Appl. 176: 114806 (2021)
• Y. Lin, J. Sun, G. Fraser, Z. Xiu, T. Liu, J. S. Dong. Recovering Fitness Gradients for Interprocedural Boolean Flags in Search-Based Testing (ISSTA 2020), pp. 440--451
• K. Wang, J. Zhang, G. Bai, R. K. L. Ko, J. S. Dong: It's Not Just the Site, It's the Contents: Intra-domain Fingerprinting Social Media Websites Through CDN Bursts. WWW 2021: 2142-2153
• H. Wang, Y. Lin, Z. Yang, J. Sun, Y. Liu, J. Dong, Q. Zhen, and T. Liu. Explaining Regressions via Alignment Slicing and Mending (TSE 2019).
• P. Kumar, Y. Lin, G. Bai, A. Parvard, A. Martin, J. Dong. Smart Grid Metering Networks: A Survey on Security, Privacy and Open Research Issues. IEEE Communications Surveys and Tutorials (COMST 2019, IF: 20.34).
• Y. Lin, J. Sun, L. Tran, G. Bai, H. Wang, J. S. Dong. Break the Dead End of Dynamic Slicing: Localizing Data and Control Omission Bug. The 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2018), pp. 509-519.
• G. Bai, Q. Ye, Y. Wu, H. Botha, J. Sun, Y. Liu, J. S. Dong, W. Visser: Towards Model Checking Android Applications. IEEE Trans. Software Eng. 44(6): 595-612 (2018)
• L. Li, J. Sun, Y. Liu, M. Sun, J. S. Dong: A Formal Specification and Verification Framework for Timed Security Protocols. IEEE Trans. Software Eng. 44(8): 725-746 (2018)
• Y. Lin, G. Meng, Y. Xue, Z. Xing, J. Sun, X. Peng, Y. Liu, W. Zhao, J. Dong. Mining Implicit Design Templates for Actionable Code Reuse. The 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2017), pp. 394-404.
• Y. Lin, J. Sun, Y. Xue, Y. Liu, J. Dong. Feedback-based Debugging. The 39th ACM SIGSOFT International Conference on Software Engineering (ICSE 2017), pp. 393-403.
• T. Tan, M. Chen, J. Sun, Y. Liu, É. André, J. S. Dong. Optimizing Selection of Competing Services with Probabilistic Hierarchical Refinement. The 38th International Conference on Software Engineering (ICSE 2016), Austin, TX, May, 2016. (accepted)
• T. Wang, J. Sun, Y. Liu, Y. Si, J.S. Dong, X. Li. A Systematic Study on Non-Zenoness Checking for Timed Automata. IEEE Transactions on Software Engineering (TSE), 41(1): 3-18 (2015).
• L. Li, J. Sun, Y. Liu, J. S. Dong: Verifying Parameterized Timed Security Protocols. FM 2015: 342-359
• J. S. Dong, L. Shi, L. Chuong, K. Jiang, J. Sun: Sports Strategy Analytics Using Probabilistic Reasoning. ICECCS 2015: 182-185
• T. Tan, Y. Xue, M. Chen, J. Sun, Y. Liu, J. S. Dong: Optimizing selection of competing features via feedback-directed evolutionary algorithms. ISSTA 2015: 246-256
• L. Gui, J. Sun, Y. Liu, J. S. Dong: Reliability assessment for distributed systems via communication abstraction and refinement. ISSTA 2015: 293-304
• É. André, Y. Liu, J. Sun, J. S. Dong. Parameter Synthesis for Hierarchical Concurrent Real-Time Systems. Real-Time System journal, 50(5-6): 620-679 (2014).
• Y. Liu, J. Sun, J. S. Dong, J. Biswas, M. Mokhtari. Towards Formal Modeling and Verification of Pervasive Computing Systems. Transactions on Computational Collective Intelligence, XVI: 62-91, Springer, 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), 40(2): 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, 44(2): 176-202 (2014)
• S. Song, J. Zhang, Y. Liu, M. Auguston, J. Sun, J. S. Dong, T. Chen. Formalizing and Verifying Stochastic System Architectures Using Monterey Phoenix, Software and Systems Modeling (SSM) journal, Springer, April 2014.
• J. S. Dong, Y. Liu, J. Sun, X. Zhang. Towards verification of computation orchestration. Formal Aspects of Computing (FAOC). Springer, 26(4): 729-759 (2014)
• Y. Liu, W. Chen, Y. A. Liu, J. Sun, S. Zhang and J. S. Dong.Verifying Linearizability via Optimized Refinement Checking. IEEE Transactions on Software Engineering (TSE), 39(7):1018-1039, 2013.
• L. Gui, J. Sun, Y. Liu, Y. Si, J. S. Dong and X. Wang. Combining Model Checking and Testing with an Application to Reliability Prediction and Distribution. The International Symposium in Software Testing and Analysis (ISSTA 2013) , Lugano, Switzerland, 15-20 July 2013.
• É. André, Y. Liu, J. Sun, J. S. Dong and S. Lin. Parameter Synthesis for Hierarchical Concurrent Real-Time Systems. The 25th International Conference on Computer Aided Verification (CAV 2013), Saint Petersburg, Russia, July, 2013.
• T. H. Tan, E. Andre, J. Sun, Y. Liu, J. S. Dong and M. Chen. Dynamic Synthesis of Local Time Requirement for Service Composition. The 35th International Conference on Software Engineering (ICSE 2013), San Francisco, USA, May, 2013
• G. Bai, J. Lei, G. Meng, S. Venkatraman, P. Saxena, J. Sun, Y. Liu, and J. S. Dong. AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations. Proceedings of the Network and Distributed System Security Symposium, NDSS 2013, San Diego, California, USA, February 24-27, 2013
• J. Sun, Y. Liu, J. S. Dong, Y. Liu, L. Shi and E. Andre. Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP. ACM Transactions on Software Engineering and Methodology (TOSEM), 22(1):3:1-3:29, 2013.
• S-W. Lin, Y. Liu, J. Sun, J. S. Dong and E. Andre. Automatic Compositional Verification of Timed Systems. The 18th International Symposium on Formal Methods (FM'12), Paris, France, Auguest 27 - 31, 2012.
• T. K. Nguyen, J. Sun, Y. Liu, J. S. Dong and Y. Liu. Improved BDD-based Discrete Analysis of Timed Systems. The 18th International Symposium on Formal Methods (FM'12), Paris, France, Auguest 27 - 31, 2012.
• S. Song, J. Sun, Y. Liu, and J. S. Dong. A Model Checker for Hierarchical Probabilistic Real-time Systems. 24th International Conference on Computer Aided Verification (CAV 2012), Berkeley, California, USA, July 7-13, 2012.
• S. Song, J. Hao, Y. Liu, J. Sun, H. Leung, and J. S. Dong. Analyzing Multi-agent Systems with Probabilistic Model Checking Approach. The 34th International Conference on Software Engineering (ICSE 2012), New Ideas and Emerging Results (NIER), Zurich, Switzerland, June 2 - 9, 2012.
• S. Zhang, J. Sun, J. Pang, Y. Liu and J. S. Dong. On Combining State Space Reductions with Global Fairness Assumptions. The 17th International Symposium on Formal Methods (FM 2011), pages 432 - 447, Lero, Limerick, Ireland, June 20 - 24, 2011.
• N. N. Tun, J. S. Dong and S. Tojo. A philosophy-driven entity classification and enrichment for ontology mapping. Expert Systems, Volume 28(2), pages 138 - 166, Willey, May 2011.
• C. Chen, J. S. Dong, J. Sun and A. Martin. A Verification System for Interval-based Specification Languages, ACM Transactions on Software Engineering and Methodology (TOSEM). 19(4), pages 1 - 36, ACM. 2010.
• H. Liang, J. S. Dong, J. Sun and W. E. Wong. Software monitoring through formal specification animation, Innovations in Systems and Software Engineering, A NASA Journal. Volume 5, Issue 4, pages 231-241, Springer, December 2009.
• C. Chen, J. S. Dong and J. Sun. A Formal Framework for Modeling and Validating Simulink Diagrams. Formal Aspects of Computing. vol. 21(5), pp 451-483, 2009.
• J. Sun, Y. Liu, J. S. Dong and J. Pang. PAT: Towards Flexible Verification under Fairness. The 21th International Conference on Computer Aided Verification (CAV 2009), Grenoble, France, June 2009.
• J. Sun, Y. Liu, A. Roychoudhury, S. Liu and J. S. Dong. Fair Model Checking with Process Counter Abstraction. The 16th International Symposium on Formal Methods (FM 2009). pages 123 - 139, Eindhoven, the Netherlands, November, 2009.
• J. S. Dong, P. Hao, S. C. Qin, J. Sun and Y. Wang, Timed Automata Patterns. IEEE Transactions on Software Engineering, vol. 34(6), pp 844-859, Nov./Dec. 2008.
• S. Ferndriger, A. Bernstein, J. S. Dong, Y. Z. Feng, Y. F. Li and J. Hunter. Enhancing Semantic Web Services with Inheritance, 7th International Semantic Web conference (ISWC'08), Karlsruhe, Germany, pp 162-177, 2008.
• N. N. Tun and J. S. Dong. Ontology Generation through a Fusion of Partial Reuse and Relation Extraction, 11th International Conference on Principles of Knowledge Representation and Reasoning (KR'08), pp 318-328, 2008.
• C. Chen, J. S. Dong and J. Sun. A Verification System for Timed Interval Calculus, The 30th International Conference on Software Engineering (ICSE'08), pp 271-280, 2008.
• K. Taguchi and J. S. Dong. Formally Specifying and Verifying Mobile Agents : Model Checking Mobility, International Journal of Agent-Oriented Software Engineering, vol2(4):449-474, 2008.
• J. S. Dong, Y. Feng and H-F. Leung, A Verification Framework for Agent Knowledge. ICFEM 2007: 57-75
• J. Sun and J. S. Dong, Design Synthesis from Interaction and State-based Specifications. IEEE Transactions on Software Engineering, Vol-32(6):349-364, 2006
• H. Wang, J. S. Dong, J. Sun and J. Sun. Reasoning Support for Semantic Web Ontology Family Languages Using Alloy. International Journal of Multiagent and Grid Systems, IOS press, Vol-2(4):455-471, 2006.
• L. Yuan, J. S. Dong, J. Sun and H. A. Basit. Generic Fault Tolerant Software Architecture Reasoning and Customization. IEEE Transactions on Reliability. Vol-55(3):421-435, 2006
• J. Sun, J. S. Dong, S. Jarzabek and H. Wang. CAD System Family Architecture and Verification: An Integrated Formal Approach. IEE Proceedings Software. Vol-153(3):102-112, 2006.
• J. S. Dong, P. Hao, X. Zhang, and S. Qin, HighSpec: a Tool for Building and Checking OZTA Models. 28th International Conference on Software Engineering (ICSE'06). 2006.
• D. Lucanu, Y.F. Li, J.S. Dong: Semantic Web Languages - Towards an Institutional Perspective. Essays Dedicated to Joseph A. Goguen, LNCS Springer, 2006: 99-123
• H. Liang, J. S. Dong, J. Sun, R. Duke, R. E. Seviora: Formal Specification-based Online Monitoring. ICECCS 2006: 152-162
• J. S. Dong, Y. Liu, J. Sun, X. Zhang: Verification of Computation Orchestration Via Timed Automata. ICFEM 2006: 226-245
• J. S. Dong, P. Hao, J. Sun, X. Zhang: A Reasoning Method for Timed CSP Based on Constraint Solving. ICFEM 2006: 342-359
• J. S. Dong: From semantic web to expressive software specifications: a modeling languages spectrum. ICSE 2006: 1063-1064
• J. Sun and J. S. Dong, Synthesis of Distributed Processes from Scenario-based Specifications. Formal Methods 2005 (FM'05), LNCS, pp 415-431, Newcastle, UK. 2005.
• J. S. Dong, R. Duke and P. Hao, Integrating Object-Z with Timed Automata . ICECCS'05:488-497, 2005. (pdf)
• J. Sun and J. S. Dong, Model Checking Live Sequence Charts. ICECCS'05:529-538, 2005.
• J. S. Dong, P. Hao, S. Qin, J. Sun and Y. Wang, Timed Patterns: TCOZ to Timed Automata. The 6th International Conference on Formal Engineering Methods (ICFEM'04), editors: J. Davies, W. Schulte and M. Barnett, LNCS, pp 483-498, Seattle. 2004.
• X. Wang, D. Zhang, J. S. Dong, C. Chin and S. Hettiarachchi. Semantic Space: A Semantic Web Infrastructure for Smart Spaces. IEEE Pervasive Computing, 3(3):32-39, July-September 2004. (pdf)
• J. S. Dong, C. Lee, H. Lee, Y. F. Li and H. Wang. A Combined Approach to Checking Web Ontologies. 13th ACM International World Wide Web Conference (WWW'04), refereed track, ACM Press, pages 714-722, NYC, USA, 2004. ( pdf )
• J. S. Dong, C. Lee, Y. F. Li and H. Wang, Verifying DAML+OIL and Beyond in Z/EVES. The 26th International Conference on Software Engineering (ICSE'04), ACM/IEEE Press, pp 201-210, Edinburgh, 2004.
• J. S. Dong. Software Modeling Techniques and the Semantic Web. The 26th International Conference on Software Engineering (ICSE'04), ACM/IEEE Press, Edinburgh, Scotland, 2004. (tutorial, slides in ps.Z (compressed ps file) or pdf )
• J. S. Dong, S. C. Qin and J. Sun. Generating Message Sequence Charts from an Integrated Formal Specification Language The 4th International Conference on Integrated Formal Methods, editors: E. Bioten, J. Derrick and G. Smith, LNCS, Springer-Verlag, pp 168-186, Canterbury, UK, 2004.
• J. S. Dong, J. Sun and H. Wang. Checking and Reasoning about Semantic Web through Alloy. 12th International Symposium on Formal Methods Europe (FM'03). editors: K. Araki, S. Gnesi and D. Mandrioli, LNCS, pages 796-813, Springer-Verlag, Pisa, Italy, 2003.
• S. Qin, J. S. Dong and W. N. Chin. A Semantic Foundation of TCOZ in Unifying Theory of Programming. FM'03. LNCS, pages 321-340, 2003.
• M. Utting, I, Toyn, J. Sun, A. Martin, J. S. Dong, N. Daley and D. Currie. ZML: XML Support for Standard Z. 3rd International Conference of Z and B Users (ZB'03), LNCS, Springer-Verlag, pages 437-456, Turku, Finland, 2003.
• B. Mahony and J.S. Dong. Deep Semantic Links of TCSP and Object-Z: TCOZ Approach. Formal Aspects of Computing journal, 13:142-160, Springer, 2002.
• J. Sun, J. S. Dong, J. Liu and H. Wang. A Formal Object Approach to the Design of ZML. Annals of Software Engineering: An international journal, 13:329-356, Kluwer Academic Publishers, 2002.
• J. S. Dong, J. Sun and H. Wang. Semantic Web for Extending and Linking Formalisms. Formal Methods Europe (FME'02 - FLoC), LNCS, Springer-Verlag, pages 587-606, Copenhagen, 2002. (pdf)
• J. Sun, J. S. Dong, J. Liu and H. Wang. Object-Z Web Environment and Projections to UML. 10th ACM International World Wide Web Conference (WWW'01), refereed track, pages 725-734, ACM Press, HK, 2001.
• J. S. Dong, State, Event, Time and Diagram in System Modeling, 23th International Conference on Software Engineering (ICSE'01), pages 733-734, IEEE Press, Toronto, 2001. ( pdf , tutorial slides in pdf )
• B. Mahony and J.S. Dong. Timed Communicating Object Z. IEEE Transactions on Software Engineering, 26(2):150-177, Feb 2000. (pdf)
• B. Mahony and J.S. Dong. Sensors and Actuators in TCOZ. World Congress on Formal Methods (FM'99), editors: J. Wing, J. Woodcock and J. Davies. LNCS, Vol 1709, pages 1166-1185, Springer-Verlag, Toulouse, France, 1999. (pdf)
• J.S. Dong, B. Mahony and N. Fulton. Modeling Aircraft Mission Computer Task Rates , World Congress on Formal Methods (FM'99), 1999.
• B. Mahony and J.S. Dong. Blending Object-Z and Timed CSP: An introduction to TCOZ. In Proceedings of the 20th International Conference on Software Engineering (ICSE'98), IEEE Press, pages 95-104, Kyoto, Japan, 1998. (postscript).
• J.S. Dong, R. Duke and G. Rose. An Object-Oriented Denotational Semantics of A (block-structured sequential) Programming Language. Object-Oriented Systems (OOS) journal 4(1):29-52, Chapman Hall, 1997.
• J.S. Dong and R. Duke. A Formal Object Model of an Object-Oriented Programming Language. In Proceedings of the 20th International Conference on Technology of Object-Oriented Languages and Systems (TOOLS'USA96), Santa Barbara, USA, 1996.
• J.S. Dong and R. Duke. The Geometry of Object Containment. Object-Oriented Systems (OOS) journal 2(1):41-63, Chapman Hall, 1995. (pdf)
• J.S. Dong. Living with Free Type and Class Union. In Proceedings of the 1995 Asia-Pacific Software Engineering Conference (APSEC'95), pages 304-312, IEEE Press, Brisbane, Australia, 1995. (postscript)
• J.S. Dong, G. Rose and R. Duke. The Role of Secondary Attributes in Formal Object Modelling. In Proceedings of the First IEEE International Conference on Engineering Complex Computer Systems (ICECCS'95). pages 31--38, Ft. Lauderdale, USA, IEEE Press, 1995. (pdf)
• J.S. Dong and R. Duke. Exclusive Control within Object Oriented Systems. In Proceedings of the 18th International Conference on Technology of Object-Oriented Languages and Systems (TOOLS'Pacific95). Melbourne, Australia, pages 123-132, Prentice-Hall, 1995. (pdf)
• J.S. Dong and R. Duke. An Object-Oriented Approach to the Formal Specification of ODP Trader. In Open Distributed Processing, II,  IFIP Transactions C: Communication Systems, C-20:341-352, North-Holland, 1994. (postscript)
• J.S. Dong, R. Duke and G. Rose. An Object-Oriented Approach to the Semantics of Programming Languages, Australian Computer Science Communications, 16(1):767-775, 1994. (postscript)
• J.S. Dong and R. Duke. Class Union and Polymorphism. In Proceedings of the 12th International Conference on Technology of Object-Oriented Languages and Systems, pages 181-190, Prentice-Hall, 1993. (postscript)

PhD Thesis

• J.S. Dong Formal Object Modelling Techniques and Denotational Semantics Studies. Computer Science Department, The University of Queensland, October 1995. thesis info , (postscript)

Keynote/Invited-Talk/Tutorial...:

• J. S. Dong, Keynote: Dependable Intelligence and Reasoning Beyond ChatGPT+ with an Application to Sports Analytics, The 6th IEEE World Symposium on Software Engineering, Kyoto, Sep 2024
• J. S. Dong, Keynote: Dependable Intelligence and Reasoning Beyond LLM, CCF Conference on Programing and AI, Dali, Dec 2024.
• J. S. Dong, Distinguished Talk: Trusted AI for Sports Analytics. Systems Engineering Workshop for Complex Intelligent Systems, May, 2024, Hong Kong Science Park. Chaired by M. Xie and J. Sifakis (2007 Turing Award)
• J. S. Dong, Keynote: Trusted AI and Reasoning beyond ChatGPT, International Multi-Conference on ¿Advances in Information Technology, Communication and Energy Systems¿ (AITCES), Bengaluru, India, January 2024.
• J. S. Dong, Keynote: Probabilistic Reasoning for Sports Analytics, 27th ICECCS, Toulouse, France, June 2023
• J. S. Dong, Keynote: Probabilistic Model Checking for Sports Strategy Analytics, SETTA. Nanjing, 2023
• J. S. Dong, Keynote: Trusted Decision Making and Dependable Intelligence, 19th International Conference On Smart Living and Public Health (ICOST), Paris, France, June 2022
• J. S. Dong, Keynote: Trusted Decision Making, ICNSC 2020 : IEEE International Conference on Networking, Sensing and Control, 2020.
• J. S. Dong, Keynote: Trusted Decision Making and Dependable Intelligence, AI-Expo, Suzhou, China, May, 2019
• J. S. Dong, Keynote: Decision Making via Model Checking, Smart Digital Futures SDF-18, June, 2018
• J. S. Dong, Invited Talk: Event-Strategy Analytics, Mathworks Summit, Tokyo, Oct, 2017
• J. S. Dong, Keynote: Event Analytics, Australian System Safety Conference, Sydney, May 2017
• J. S. Dong, Invited Annual Lecture: Model Checking and Event Analytics, The Engineering Australia Annual ITEE/IET Informatics Lecture, Brisbane, March 2017.
• J. S. Dong, Keynote: Event-Strategy Analytics, 9th International Symposium on Theoretical Aspects of Software Engineering (TASE'15), September 12-14, 2015, Nanjing, China
• J. S. Dong, Invited Talk: Event Analytics, 11th International Colloquium on Theoretical Aspects of Computing, 17-20 Sep 2014, Bucharest, Romania.
• J. S. Dong, Tutorial: Pervasive Model Checking: PAT Approach, 11th International Colloquium on Theoretical Aspects of Computing, 17 Sep 2014, Bucharest, Romania.
• J. S. Dong, Invited Talk: Pervasive Model Checking and Event Analytics, Second International Seminar on Program Verification, Automated Debugging and Symbolic Computation, Beijing, Oct 23-25, 2013
• J. S. Dong, J. Sun and Y. Liu. Tutorial: Build Your Own Model Checker in One Month. 35th International Conference on Software Engineering (ICSE 2013), San Francisco, USA, May 18, 2013
• J. S. Dong, Invited Talk: Pervasive Model Checking, MSR Verified Software Workshop and Summer School (Co-Chairs: Tony Hoare and Jifeng He), Shanghai, July 2012.
• J. S. Dong, J. Sun and Y. Liu. Tutorial: Build Your Own Model Checker in One Month. The 17th International Symposium on Formal Methods (FM 2011), Limerick, Ireland, June 20, 2011.
• J. S. Dong, Invited Talk: Expressive Design Techniques and Pervasive Model Checking, GRACE International symposium on Advanced Software Engineering, NII, Tokyo, Japan. March 2010.
• J. S. Dong and J. Sun. Invited Tutorial: Towards Expressive Specification and Efficient Model Checking, 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China. July 2009.
• J. S. Dong, Invited Talk: A Spectrum of Modeling languages and Transformations. The Fourth Workshop on Programmable Structured Documents, University of Tokyo, Japan, Dec 2005.
• J. S. Dong, Half-Day Tutorial: Modeling Languages Spectrum: From Web Ontology to Behaviour Specifications, Formal Methods 2005 (FM'05), University of Newcastle upon Tyne, UK. July 2005.
• J. S. Dong, Invited Talk: Formal Designs for Embedded and Hybrid Systems, International Conference on Embedded and Hybrid Systems (IEHSC), Singapore, May 2005.
• J. S. Dong, Keynote: Semantic Web in Action - Modeling and Verification, 4th International Conference on Internet Information Retrieval (ICIIR'04), Nov, Seoul, Korea, 2004.
• J. S. Dong. Full-Day Tutorial: Software Modeling Techniques and the Semantic Web. The 26th International Conference on Software Engineering (ICSE'04), ACM/IEEE Press, Edinburgh, Scotland, 2004. (slides in ps.Z (compressed ps file) or pdf )
• J. S. Dong, Half-Day Tutorial: Semantic Web and Formal Methods. 12th International Symposium on Formal Methods Europe (FM'03). Pisa, Italy, 2003. Slides in ( ps or ( pdf )
• J.S. Dong, Full-Day Tutorial: Integrated Formal Modeling Techniques and UML, 23rd International Conference on Software Engineering (ICSE'01), Toronto, Canada, 2001. ( slides with solutions in pdf )

PhD/MSc Students

Current

• Dileepa Fernando, Probabilistic Model Checking Game Theory Based Systems
• Kulani Tharaka Mahadewa, IoT Security of Smart Home Systems
• JIANG Kan, Sports Analytics

Completed/Submitted

• SUN, Jing (PhD 2003, -> Associate Professor with tenure at The University of Auckland, NZ)
• WANG, Hai (PhD 2004, -> Lecturer at Aston University, UK)
• SUN, Jun (PhD 2006, -> Full Professor at Singapore Management University)
• LI, Yuanfang (PhD 2006, -> Associate Professor at Monash University, Australia
• HAO, Ping (PhD 2008, -> Tech Lead, Prudential Service Singapore)
• YUAN, Ling (PhD 2008, -> Full Professor at Huazhong University of Science and Technology, China)
• LIANG, Hui (PhD 2008, -> Lead Data Scientist, Innovation Center, HP Enterprise, Singapore)
• CHEN Chunqing (PhD 2009, -> Researcher at HP Research Lab, Singapore)
• LIU, Yang (PhD 2010, -> Full Professor at Nanyang Technological University)
• FENG Yuzhang (PhD 2011, -> First Vice President (Analytics Strategy) at United Overseas Bank Limited (UOB))
• ZHANG, Xian (PhD 2012, Postdoc at I2R-NUS Research Project)
• SHI Ling (PhD 2012, -> Research Manager at NTU)
• ZHANG Shaojie (PhD 2013, -> Software Engineer, Google, Canada)
• ZHENG Manchun (PhD 2013, -> Member of Technical Staff at Pure Storage, CA, USA)
• SONG SongZheng (PhD 2013, -> Research Fellow at NTU)
• TAN Tian Huat (PhD 2013, -> Data Scientist at IBM)
• LIU Yan (PhD 2014, -> Postdoc at Tlab-NUS)
• GUI Lin (PhD 2014, -> Vice President of Data Science at Lazada Group)
• NGUYEN Truong Khanh (PhD 2014, -> Senior Engineer at Autodesk)
• LIU Shuang (PhD 2015, -> Associate Professor, Tianjin University)
• Chen Manman, (PhD 2015, -> Data Scientist at Autodesk)
• BAI Guangdong (PhD 2015, -> Associate Professor, University of Queensland)
• LI Li (PhD 2015, -> Engineering Manager at Apple)
• Ye Quanqi (PhD 2018, -> Lecturer at Waikato University)
• WONG Kailong (PhD 2021, -> Associate Professor at Huazhong University of Science and Technology, China
• LUU Anh Tuan (MSc, -> Assistant Professor at NTU)
• WANG, Xiaohang (MSc, co-advisor, -> Google (New York City Lab))
• Huang, Xiaoning (MSc)
• TANG, Yue Linda (MSc)
• WANG, Yan (MSc)
• LIU, Jing (MSc)
• ONG, Wai Chun West Jean (MSc, co-advisor)
• TEH, Hsin Yee (MSc, co-advisor)

Useful things to know about PhD research:
Oxford University Computing Lab (preparation in pdf) ,
H.T. Kung Harvard University
M. Bellare, UCSD

Note: I am currently interested in taking new PhD students. Contact me only if you are very interested in formal methods and are exceptionally strong in discrete maths and logic. If you are one of the top students from a very good university, there is an excellent phd scholarship at NGS.

Computer Science Department School of Computing