YAHUI SONG (宋雅辉) I am currently a Software Developer @ Core Strats, Standard Chartered Bank [Github] [Google Scholar] Email: yahui DOT song AT u DOT nus DOT edu I was a Research Fellow in the Automated Program Repair group at NUS, working with Professor Abhik Roychoudhury. I defended my PhD in May 2023 at the School of Computing (Soc), NUS, supervised by Associate Professor Wei-Ngan Chin. I received my Master's degree from NUS in 2018, and my Bachelor's degree in computer science from Sun Yat-sen University, China, in 2017. My research interests are: specification and verification, program analyses, automated program repair, temporal logic, and separation logic.

Talk

• (25/06/2025) I gave a (zoom) talk upon Future Conditions: Temporal Property guided Program Analysis, Repair and Verification with Prof. Yulei Sui's group at UNSW!
• (04/12/2024) I presented our ongoing work on CTL repair at SG Programming Languages Summit!
• (12/10/2024) I gave a (zoom) talk about ProveNFix and Future-conditions with Prof. Yun Lin's group at Shanghai Jiao Tong University!
• (13/09/2024) I gave a talk at ETH Zürich with Prof. Zhendong Su's Group. Great time talking to Zu-Ming, Jinsheng, Hao, Chengyu, Dominik and Shaohua!
• (09/09/2024) I gave a talk at the EPFL PL Seminar, hosted by Prof. Viktor Kunčak. It was a great opportunity to meet faculty and students! Great time talking to Clément, Aurèle, Thomas, Sankalp, Yawen, Shardul and Samuel.
• (06/09/2024) I gave a talk at ETH Zürich with Prof. Peter Müller's Group. Great time talking to Michael, Marco, João, and Felix!
• (13/11/2022) I gave a (zoom) talk about my PhD thesis at the Languages, Systems, and Data (LSD) Seminar at UCSC, hosted by Prof. Lindsey Kuper!

Peer-reviewed Research Paper

• TSE2026. "Computation Tree Logic Guided Program Repair" [paper] [artifact]
  by Yu Liu*,Yahui Song*, Martin Mirchev, Abhik Roychoudhury
  IEEE Transactions on Software Engineering.
  
  
• SAS2025. "Specifying and Verifying Future Conditions" [pdf] [artifact] [code] [slides] [specs]
  by Yahui Song, Darius Foo, Wei-Ngan Chin.
  The 32nd Static Analysis Symposium, Singapore.
  
  
• TACAS2025. "Inferring Incorrectness Specifications for Object-Oriented Programs" [pdf]
  by Wenhua Li, Quang Loc Le, Yahui Song, Wei-Ngan Chin.
  The 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Hamilton, Canada.
  
  
• ICFP2024. "Specification and Verification for Unrestricted Algebraic Effects and Handling" [pdf] [appendix] [code] [slides]
  by Yahui Song, Darius Foo, Wei-Ngan Chin.
  The 29th ACM SIGPLAN International Conference on Functional Programming, Milan, Italy.
  
  
• FM2024. "Staged Specification Logic for Verifying Higher-Order Imperative Programs" [pdf] [appendix] [code]
  by Darius Foo, Yahui Song, Wei-Ngan Chin.
  The 26th International Symposium on Formal Methods, Milan, Italy.
  Our "Staged Logic" has now been fully formalized in Coq, thanks to Darius!
  
  
• FSE2024. "ProveNFix: Temporal Property guided Program Repair" [pdf] [appendix] [code] [artifact] [slides]
  by Yahui Song, Xiang Gao, Wenhua Li, Wei-Ngan Chin, Abhik Roychoudhury.
  The ACM International Conference on the Foundations of Software Engineering, Porto de Galinhas, Brazil.
  ACM SIGSOFT Distinguished Paper Award
  
  
• APLAS2023. "Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection" [pdf] [slides]
  by Wenhua Li, Quang Loc Le, Yahui Song, Wei-Ngan Chin.
  The 21st Asian Symposium on Programming Languages and Systems, Taipei.
  
  
• TACAS2023. "Automated Verification for Real-Time Systems" [pdf] [slides] [code] [proofs]
  by Yahui Song, Wei-Ngan Chin.
  The 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Paris, France.
  
  
• APLAS2022. "Automated Temporal Verification for Algebraic Effects" [pdf] [slides] [code]
  by Yahui Song, Darius Foo, Wei-Ngan Chin.
  The 20th Asian Symposium on Programming Languages and Systems, Auckland, New Zealand.
  
  
• VMCAI2021. "A Synchronous Effects Logic for Temporal Verification of Pure Esterel" [pdf] [slides] [code] [demo]
  by Yahui Song, Wei-Ngan Chin.
  The 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, Online.
  
  
• ICFEM2020. "Automated Temporal Verification of Integrated Dependent Effects" [pdf] [slides] [code] [demo]
  by Yahui Song, Wei-Ngan Chin.
  The 22nd International Conference on Formal Engineering Methods, Singapore.
  
  

Theses and Preprints

• Arxiv. "Detecting LLM Fact-conflicting Hallucinations Enhanced by Temporal-logic-based Reasoning" [pdf]
  by Ningke Li*, Yahui Song*, Kailong Wang, Yuekang Li, Ling Shi, Yi Liu, Haoyu Wang
  
  
• PhD Thesis. "Symbolic Temporal Verification Techniques with Extended Regular Expressions" [pdf] [slides]
  Degree of Doctor of Philosophy, Department of Computer Science, National University of Singapore.
  Supervisor: Wei-Ngan Chin.
  Committee: Joxan Jaffar, Jin Song Dong.
  
  
• Manuscript. "Automated Temporal Verification for Preemptive Asynchronous Programs" [pdf] [code]
  by Yahui Song, Wei-Ngan Chin.
  
  
• Manuscript. "An SQL Frontend on top of OCaml for Data Analysis" (Presented in IFL2022) [pdf] [slides] [code]
  by Yan Dong, Yahui Song, Wei-Ngan Chin.
  The 34th Symposium on Implementation and Application of Functional Languages, Copenhagen, Denmark.
  
  
• Master Thesis. "Programming Abstraction for IoT Devices" [pdf] [demo]
  Degree of Master of Computing, Department of Computer Science, National University of Singapore.
  Supervisor: Wei-Ngan Chin, co-supervised by Mahmudul Faisal Al Ameen.
  Committee: Siau-Cheng Khoo, Hugh Anderson.
  
  

Service

• Program Committee of TOSEM'25, ICSE'26, ICFP'25, SRC@SPLASH'25, HOPE'25, OCaml'25, APR@ICSE'25, TASE'24 and its Special Journal Issue, STTT'21 (RV'21 Special Journal Issue).
• Artifact Evaluation Committee of: CAV'23, CAV'22, PLDI'22, POPL'22, ESOP'22.
• Subreviewer of: POPL'22.
• PLDI'19 PLMW Scholarship, Student Volunteering in Phoenix, Arizona, United States.

Student Research Competition

• SPLASH2022. "Automated Verification for Real-Time Systems using Implicit Clocks and an Extended Antimirov Algorithm" [poster] [pdf] [code] [certificate]
  by Yahui Song, Wei-Ngan Chin.
  SPLASH SRC, Auckland, New Zealand.
  
  
• APLAS2019. "Automated Temporal Verification via Rewriting Conditional Dependent Effects" [pdf]
  by Yahui Song, Wei-Ngan Chin.
  The 17th Asian Symposium on Programming Languages and Systems, Indonesia.
  
  
• APLAS2018. "Arrowrized Abstraction for IOT programs" [pdf]
  by Yahui Song, Wei-Ngan Chin.
  The 16th Asian Symposium on Programming Languages and Systems, New Zealand.
  First Prize Student Research Competition
  
  

Teaching Experience

• I am the TA for IT5100A: Typed Functional Programming in Practice with Dr. Wei-Ngan Chin and Dr. Razvan Voicu.
  - Semester 2, 2021/2022.
• Honor List of Student Tutors for Excellence of Teaching, 2020-2021. [certificate]
• TA for TIC2701: Principles of Programming Languages with Dr. PRABAWA Adi Yoga Sidi.
  - Semester 1, 2020/2021. [feedback report]
• TA for CS2104: Programming Language Concepts with Dr. Wei-Ngan Chin.
  - Semester 1, 2020/2021. [feedback report]
• Grader for YSC1212 in Yale-NUS College: Introduction to Computer Science with Dr. Aquinas Hobor.
  - Semester 1, 2020/2021.
• TA for CS4215: Programming Language Implementation with Dr. Razvan Voicu.
  - Semester 2, 2018/2019.
• TA for CS3203: Software Engineering Project with Dr. ZHAO Jin and Dr. Cristina CARBUNARU.
  - Semester 2, 2020/2021.
  - Semester 1 & 2, 2019/2020. [feedback report]
  - Semester 2, 2018/2019. [feedback report]
• TA for CS3219: Software Engineering Principles and Patterns with Dr. Bimlesh WADHWA.
  - Semester 1, 2020/2021.
  - Semester 1 & 2, 2019/2020.
  - Semester 1, 2018/2019.
  - Semester 1, 2017/2018.

More

• INTERNSHIP. I did an exciting internship in the Security lab of Huawei in Singapore, supervised by Dr. Shengchao Qin and co-supervised by Dr. Mengda He. [Certificate]
• NUS Soc Research Week 2021 Presentation in Singapore. [demo] [slides]
• The 31st symposium on Implementation and Application of Functional Languages Draft Paper for Presentation in NUS, Singapore. [slides]
• NUS Soc Research Week 2019 Presentation in Singapore. [slides]
• HACKATHON. GSAC 2018 Singapore Hackathon (ALIBABA & LAZADA): scheduling algorithm competition (First Prize).
• Papers that I am reading:
  Robustifying Debug Information Updates in LLVM via Control-Flow Conformance Analysis
  Modal Effect Types
  A Complete Approach to Loop Verification with Invariants and Summaries
  Improvements in Software Verification and Witness Validation: SV-COMP 2025