Yong Kiam Tan

About

I also hold a joint appointment as a Nanyang Assistant Professor at the College of Computing and Data Science, NTU, Singapore.

I completed my PhD in Computer Science (Pure and Applied Logic) at Carnegie Mellon University, where I was supported by a National Science Scholarship (BS-PhD) from A*STAR, Singapore.

I am an alumnus of the Logical Systems Lab, where I was fortunate to be advised by Prof. André Platzer.

News

• I am co-organizing the SG PL summit with Prof. Ilya Sergey. Please consider attending and giving a talk.

• Our paper on "Formally Certified Approximate Model Counting" received a Distinguished Paper Award at CAV 2024.

• I started on a joint appointment between NTU and A*STAR (from 18 Jul 2024).

• I was awarded the Singapore NRF Fellowship Class of 2024 (link), check out the recruitment page for open positions.

• My collaborators and I have papers accepted at IJCB'24, CICM'24, and CAV'24.

• I am on the PC of TACAS 2025 and CADE-30 (held in 2025).

Recruitment

I am looking for students and postdocs to work on topics related to my research interests listed below.

Please visit the recruitment page for details.

All positions are fully funded with competitive stipends/salaries.

They are based in Singapore at the College of Computing and Data Science, NTU and at the Institute for Infocomm Research, A*STAR.

Past: Derrick Wan (NTU undergrad), Sunpill Kim (ARAP co-supervisor), Bora Jeong (SIPGA co-supervisor), James Gallicchio (CMU undergrad)

Tools / Formalizations

• I contributed to the KeYmaera X theorem prover for hybrid systems. Specifically, I developed much of its differential equations and switched systems automation.

• I am a developer of the CakeML compiler, which is formally verified in the HOL4 theorem prover.

• We are building (and maintaining) a number of verified proof checkers in CakeML, see here for more details and tool links.

• I am also a user of Isabelle/HOL, here are my AFP entries.

Publications

Please feel free to contact me for preprints if they are not available below; use the DOI links for official publications.

Please let me know if you find any broken links below or errors in my papers.

(*) indicates alphabetical author order, either of all authors or the ones indicated.

Journals

1. Verified propagation redundancy and compositional UNSAT checking in CakeML

   Yong Kiam Tan, Marijn Heule, Magnus O. Myreen

   Software Tools for Technology Transfer (STTT). Extended version of our TACAS'21 paper. (doi)

2. An Axiomatic Approach to Existence and Liveness for Differential Equations

   Yong Kiam Tan, André Platzer

   Formal Aspects of Computing (FAOC). Extended version of our FM'19 paper. (arXiv,doi)

3. Pegasus: Sound Continuous Invariant Generation

   Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer

   Formal Methods in System Design (FMSD). Extended version of our FM'19 paper. (tool,arXiv,doi,ICSE'23 Showcase slides)

4. Proof-Producing Synthesis of CakeML from Monadic HOL Functions

   Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan

   Journal of Automated Reasoning (JAR). Extended version of our IJCAR'18 paper. (link,doi)

5. Differential Equation Invariance Axiomatization

   André Platzer, Yong Kiam Tan (*)

   Journal of the ACM (JACM). Extended version of our LICS'18 paper. (preprint,arXiv,doi)

6. A Formal Safety Net for Waypoint-Following in Ground Robots

   Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, André Platzer

   IEEE Robotics and Automation Letters (RA-L). (arXiv,doi)

7. The Verified CakeML Compiler Backend

   Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, Michael Norrish

   Journal of Functional Programming (JFP). Extended version of our ICFP'16 paper. (preprint,doi)

Conferences

1. Unsupervised Fingerphoto Presentation Attack Detection With Diffusion Models

   Hailin Li, Raghavendra Ramachandra, Mohamed Ragab, Soumik Mondal, Yong Kiam Tan, Khin Mi Mi Aung

   IJCB 2024. (arXiv)

2. Formalizing Coppersmith's Method in Isabelle/HOL

   Katherine Kosaian, Yong Kiam Tan, Kristin Y. Rozier

   CICM 2024. (AFP entry,doi)

3. Formally Certified Approximate Model Counting

   Yong Kiam Tan (*), Jiong Yang (*), Mate Soos, Magnus O. Myreen, Kuldeep S. Meel

   CAV 2024. Distinguished Paper Award. (AFP entry,arXiv,doi)

4. Certified MaxSAT Preprocessing

   Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, Jakob Nordström

   IJCAR 2024. (doi)

5. End-to-End Verification for Subgraph Solving

   Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan (*)

   AAAI 2024. (doi,materials)

6. Scores Tell Everything about Bob: Non-adaptive Face Reconstruction on Face Recognition Systems

   Sunpill Kim, Yong Kiam Tan, Bora Jeong, Soumik Mondal, Khin Mi Mi Aung, Jae Hong Seo

   SP 2024. (doi)

7. Cakes that Bake Cakes: Dynamic Computation in CakeML

   Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens

   PLDI 2023. (doi)

8. A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

   Katherine Kosaian, Yong Kiam Tan, André Platzer

   CPP 2023. (AFP entry,arXiv,doi)

9. Implicit Definitions with Differential Equations for KeYmaera X (System Description)

   James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer

   IJCAR 2022. (arXiv, doi)

10. Verified Compilation and Optimization of Floating-Point Programs in CakeML

    Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox

    ECOOP 2022. (doi)

11. Verifying Switched System Stability With Logic

    Yong Kiam Tan, Stefan Mitsch, André Platzer

    HSCC 2022. Best Paper Award and Best Repeatability Evaluation Award. (arXiv,doi,slides,materials)

12. A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm

    Katherine Cordwell, Yong Kiam Tan, André Platzer

    ITP 2021. (AFP entry,arXiv,doi)

13. Switched Systems as Hybrid Programs

    Yong Kiam Tan, André Platzer

    ADHS 2021. (arXiv,doi,slides)

14. Deductive Stability Proofs for Ordinary Differential Equations

    Yong Kiam Tan, André Platzer

    TACAS 2021. (preprint,arXiv,doi,slides)

15. cake_lpr: Verified Propagation Redundancy Checking in CakeML

    Yong Kiam Tan, Marijn Heule, Magnus O. Myreen

    TACAS 2021. (tool,preprint,doi,slides)

16. Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs

    Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, Yong Kiam Tan

    PACMPL OOPSLA 2020. (preprint,doi)

17. The Poincaré-Bendixson Theorem in Isabelle/HOL

    Fabian Immler, Yong Kiam Tan (*)

    Certified Programs and Proofs (CPP'20). (AFP entry,preprint,doi,slides)

18. An Axiomatic Approach to Liveness for Differential Equations

    Yong Kiam Tan, André Platzer

    Formal Methods (FM'19). (preprint,arXiv,doi,slides)

19. Pegasus: A Framework for Sound Continuous Invariant Generation

    Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer

    Formal Methods (FM'19). Best Tool Paper Award. (tool,preprint,doi,slides,ICSE'23 Showcase slides)

20. Verified Compilation on a Verified Processor

    Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony Fox

    Programming Language Design and Implementation (PLDI'19). (preprint,doi)

21. Vector Barrier Certificates and Comparison Systems

    Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer

    Formal Methods (FM'18). (preprint,doi,slides)

22. Differential Equation Axiomatization: The Impressive Power of Differential Ghosts

    André Platzer, Yong Kiam Tan (*)

    Logic in Computer Science (LICS'18). (preprint (with appendix),arXiv,doi,slides, minor appendix corrections: 10 Jun 2019)

23. Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions

    Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish

    International Joint Conference on Automated Reasoning (IJCAR'18). (preprint,doi,slides)

24. VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models

    Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, André Platzer

    Programming Language Design and Implementation (PLDI'18). (preprint,doi)

25. Verifying Efficient Function Calls in CakeML

    Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan

    International Conference on Functional Programming (PACMPL ICFP'17). (preprint,doi)

26. Verified Compilation of CakeML to Multiple Machine-Code Targets

    Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar

    Certified Programs and Proofs (CPP'17). (preprint,doi)

27. A New Verified Compiler Backend for CakeML

    Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, Michael Norrish

    International Conference on Functional Programming (ICFP'16). (preprint,doi,slides)

28. Functional Big-Step Semantics

    Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan

    European Symposium on Programming (ESOP'16). (preprint,doi)

Workshops

1. Improved Recurrent Neural Networks for Session-based Recommendations

   Yong Kiam Tan, Xinxing Xu, Yong Liu

   DLRS'16. (preprint,doi)

2. A Verified Type System for CakeML

   Yong Kiam Tan, Scott Owens, Ramana Kumar

   IFL'15. Peter Landin Prize. (preprint,doi)

Technical Reports / Drafts

• How to Prove "All" Dfferential Equation Properties

  André Platzer, Yong Kiam Tan (*)

  CMU-CS-17-117. (link, superseded by arXiv version and LICS'18 paper)

Others

• ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving

  Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan (doi)

• ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving

  Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan. (doi)

Theses

• Deductive Verification for Ordinary Differential Equations: Safety, Liveness, and Stability

  Committee: André Platzer (Chair), Jeremy Avigad, Stefan Mitsch, Frank Pfenning, Joël Ouaknine.

  CMU-CS-22-114. CMU SCS Distinguished Dissertation Award 2022. (link)

• Verified Register Allocation for CakeML

  My undergraduate dissertation supervised by Ramana Kumar and Magnus Myreen. (link)

Review

I have sub-reviewed for the following conferences: CPP 2019, ESOP 2020, EMSOFT 2022, ICCPS 2020, 2022, ITP 2016, 2017, LICS 2019, 2020, 2023, MEMOCODE 2017, NFM 2023, iFM 2024, VMCAI 2025

I have reviewed for the following journals: Journal of Automated Reasoning, IEEE Transactions on Intelligent Vehicles

I was also on the PLDI 2020 Artifact Evaluation Committee.

Contact

Email (Personal): tanyongkiam@gmail.com

Email (A*STAR): tan_yong_kiam@i2r.a-star.edu.sg

Email (NTU): yongkiam.tan@ntu.edu.sg

Phone: (+65) 7 * (12345678 + 996193) (Email preferred)

Github: https://github.com/tanyongkiam

ORCiD: https://orcid.org/0000-0001-7033-2463

CV: please contact me through one of the methods above

FAQ

A: It was the easiest option for me. If you are unable to (efficiently) find what you are looking for on this page, please let me know.