CARVIEW

MOTORHOMES

Select Language

HTTP/2 200 server: GitHub.com content-type: text/html; charset=utf-8 last-modified: Thu, 11 Dec 2025 13:44:49 GMT access-control-allow-origin: * etag: W/"693acad1-6618" expires: Mon, 29 Dec 2025 11:13:22 GMT cache-control: max-age=600 content-encoding: gzip x-proxy-cache: MISS x-github-request-id: D6C1:444BC:8BEFAD:9D09C2:69525FFA accept-ranges: bytes date: Mon, 29 Dec 2025 11:03:22 GMT via: 1.1 varnish age: 0 x-served-by: cache-bom-vanm7210053-BOM x-cache: MISS x-cache-hits: 0 x-timer: S1767006202.466427,VS0,VE205 vary: Accept-Encoding x-fastly-request-id: 5e58a1fa64f5dfe11cb0d32fe5e085f2227f1dc8 content-length: 7589 Yong Kiam Tan

Yong Kiam Tan

About

I am a research scientist in the Cybersecurity department at the Institute for Infocomm Research, A*STAR, Singapore.

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 fortunate to be advised by Prof. André Platzer.

News

(updated 15 Nov 2025)

Our paper "Verified VCG and Verified Compiler for Dafny" was accepted at CPP 2026.
Our paper "Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables" was accepted at AAAI 2026 (poster).
I will give an invited tutorial at the Indian SAT+SMT School in December 2025.
I am co-PC chair, together with Aina Niemetz, for VSTTE'26 (co-located with FMCAD'26 in Graz, Austria).
I am on the PC of CAV and ITP 2026.

Recruitment

I am looking for students (master's, PhD) and postdocs to work on topics related to my research interests.

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 .

Please visit the recruitment page for instructions and details.

Research

I am interested in applications of deductive verification and interactive theorem proving in automated reasoning, compilers, formalized mathematics, hybrid systems, and security (cryptography).

In general, I like to learn and explore new areas of math / computer science, and theorem proving gives me a great ~~excuse~~ way to do so.

Please get in touch with me (contacts below) if you are interested in collaborating on any of these topics.

My PhD thesis examined the proof theory of Differential Dynamic Logic (dL), in particular, the continuous fragment of dL, which allows users to syntactically reason about systems of ordinary differential equations.

I work on research with "A Small Formal Methods Group", consisting of the following amazing folks:

Wei-Lin Wu (A*STAR research scientist)
Joe Watt (A*STAR research engineer)
Shuhan He (NTU PhD student)
Seng Boon Keat, Steven Octavianus Rahmat, Kum Hao Yun (NTU URECA)
Irvin Ng (TP student intern)
Visitors, Alumni, and Others.

Publications

Click to show 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

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)
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)
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)
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)
Differential Equation Invariance Axiomatization
André Platzer, Yong Kiam Tan (*)
Journal of the ACM (JACM). Extended version of our LICS'18 paper. (preprint,arXiv,doi)
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)
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

Verified VCG and Verified Compiler for Dafny
Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan
CPP'26. (to appear)
Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables
Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, Yong Kiam Tan (*)
AAAI 2026. (poster, to appear)
Certifying Projected Knowledge Compilation
Randal Bryant, Yong Kiam Tan, Marijn Heule
SAT 2025. (doi)
Efficient Certified Reasoning for Binarized Neural Networks
Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel
SAT 2025. Best Student Paper Award Runner-Up. (doi)
Practically Feasible Proof Logging for Pseudo-Boolean Optimization
Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, Marc Vinyals
CP 2025. (AFP entry,doi)
Verification of the CVM Algorithm with a Functional Probabilistic Invariant
Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan
ITP 2025. (doi)
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)
Formalizing Coppersmith's Method in Isabelle/HOL
Katherine Kosaian, Yong Kiam Tan, Kristin Y. Rozier
CICM 2024. (AFP entry,doi)
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)
Certified MaxSAT Preprocessing
Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, Jakob Nordström
IJCAR 2024. (doi)
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)
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)
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)
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian, Yong Kiam Tan, André Platzer
CPP 2023. (AFP entry,arXiv,doi)
Implicit Definitions with Differential Equations for KeYmaera X (System Description)
James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer
IJCAR 2022. (arXiv, doi)
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)
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)
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)
Switched Systems as Hybrid Programs
Yong Kiam Tan, André Platzer
ADHS 2021. (arXiv,doi,slides)
Deductive Stability Proofs for Ordinary Differential Equations
Yong Kiam Tan, André Platzer
TACAS 2021. (preprint,arXiv,doi,slides)
cake_lpr: Verified Propagation Redundancy Checking in CakeML
Yong Kiam Tan, Marijn Heule, Magnus O. Myreen
TACAS 2021. (tool,preprint,doi,slides)
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)
The Poincaré-Bendixson Theorem in Isabelle/HOL
Fabian Immler, Yong Kiam Tan (*)
Certified Programs and Proofs (CPP'20). (AFP entry,preprint,doi,slides)
An Axiomatic Approach to Liveness for Differential Equations
Yong Kiam Tan, André Platzer
Formal Methods (FM'19). (preprint,arXiv,doi,slides)
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)
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)
Vector Barrier Certificates and Comparison Systems
Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer
Formal Methods (FM'18). (preprint,doi,slides)
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)
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)
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)
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)
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)
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)
Functional Big-Step Semantics
Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan
European Symposium on Programming (ESOP'16). (preprint,doi)

Workshops

Improved Recurrent Neural Networks for Session-based Recommendations
Yong Kiam Tan, Xinxing Xu, Yong Liu
DLRS'16. (preprint,doi)
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)

Tools / Formalizations

Click to show 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.

Funding

Click to show funding.

My undergrad/PhD was supported by a National Science Scholarship (BS-PhD) from A*STAR, Singapore.
My ongoing research is supported by a Singapore NRF Fellowship, Class of 2024 (link).

Academic Service

Click to show academic service.

I was on the PC for: CPP 2024, IJCAR 2024, LPAR-25, ITP 2024, FM 2024, APLAS 2024, TACAS 2025, CADE-30, ITP 2025.

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.