YAHUI SONG (宋雅辉)

Research Fellow [Github] [Google Scholar] [CV] [Research Statement] [Teaching Statement]
Department of Computer Science
National University of Singapore (NUS)

Lab: PL&SE Research Lab B41 (COM3)
Email: yahui_s AT nus DOT edu DOT sg
Address: NUS COM3, 11 Research Link, Singapore 119391

SONG YAHUI

About Me

I am 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

Research Paper

  • 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

  • Arxiv. "Computation Tree Logic Guided Program Repair" [pdf]
    by Yu Liu*,Yahui Song*, Martin Mirchev, Abhik Roychoudhury

  • 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

Student Research Competition

Teaching Experience

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