default search action
Yong Kiam Tan
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j18]Katherine Kosaian, Yong Kiam Tan:
Formalizing Coppersmith's Method. Arch. Formal Proofs 2024 (2024) - [j17]Yong Kiam Tan, Jiong Yang:
Approximate Model Counting. Arch. Formal Proofs 2024 (2024) - [c30]Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström
, Andy Oertel
End-to-End Verification for Subgraph Solving. AAAI 2024: 8038-8047 - [c29]Yong Kiam Tan
Formally Certified Approximate Model Counting. CAV (1) 2024: 153-177 - [c28]Hailin Li, Raghavendra Ramachandra, Mohamed Ragab, Soumik Mondal, Yong Kiam Tan, Khin Mi Mi Aung:
Unsupervised Fingerphoto Presentation Attack Detection With Diffusion Models. IJCB 2024: 1-10 - [c27]Hannes Ihalainen
Certified MaxSAT Preprocessing. IJCAR (1) 2024: 396-418 - [c26]Katherine Kosaian
Formalizing Coppersmith's Method in Isabelle/HOL. CICM 2024: 127-145 - [c25]Sunpill Kim, Yong Kiam Tan, Bora Jeong, Soumik Mondal, Khin Mi Mi Aung, Jae Hong Seo:
Scores Tell Everything about Bob: Non-adaptive Face Reconstruction on Face Recognition Systems. SP 2024: 1684-1702 - [i17]Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Jakob Nordström
Certified MaxSAT Preprocessing. CoRR abs/2404.17316 (2024) - [i16]Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel:
Formally Certified Approximate Model Counting. CoRR abs/2406.11414 (2024) - [i15]Hailin Li, Raghavendra Ramachandra, Mohamed Ragab, Soumik Mondal, Yong Kiam Tan, Khin Mi Mi Aung:
Unsupervised Fingerphoto Presentation Attack Detection With Diffusion Models. CoRR abs/2409.18636 (2024) - 2023
- [j16]Emin Karayel, Yong Kiam Tan:
Concentration Inequalities. Arch. Formal Proofs 2023 (2023) - [j15]Sunpill Kim, Yong Kiam Tan:
The Schwartz-Zippel Lemma. Arch. Formal Proofs 2023 (2023) - [j14]Thomas Sewell
Cakes That Bake Cakes: Dynamic Computation in CakeML. Proc. ACM Program. Lang. 7(PLDI): 1121-1144 (2023) - [j13]Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen:
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML. Int. J. Softw. Tools Technol. Transf. 25(2): 167-184 (2023) - [c24]Katherine Kosaian
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. CPP 2023: 211-224 - 2022
- [j12]Katherine Cordwell, Yong Kiam Tan, André Platzer:
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. Arch. Formal Proofs 2022 (2022) - [j11]Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox:
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). Dagstuhl Artifacts Ser. 8(2): 10:1-10:2 (2022) - [c23]James Gallicchio
Implicit Definitions with Differential Equations for KeYmaera X - (System Description). IJCAR 2022: 723-733 - [c22]Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock
Verified Compilation and Optimization of Floating-Point Programs in CakeML. ECOOP 2022: 1:1-1:28 - [c21]Yong Kiam Tan, Stefan Mitsch, André Platzer:
Verifying Switched System Stability With Logic. HSCC 2022: 2:1-2:11 - [i14]James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer:
Implicit Definitions with Differential Equations for KeYmaera X (System Description). CoRR abs/2203.01272 (2022) - [i13]Katherine Kosaian, Yong Kiam Tan, André Platzer:
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. CoRR abs/2209.10978 (2022) - 2021
- [j10]Katherine Cordwell, Yong Kiam Tan, André Platzer:
The BKR Decision Procedure for Univariate Real Arithmetic. Arch. Formal Proofs 2021 (2021) - [j9]Yong Kiam Tan
An axiomatic approach to existence and liveness for differential equations. Formal Aspects Comput. 33(4-5): 461-518 (2021) - [j8]Andrew Sogokon
Pegasus: sound continuous invariant generation. Formal Methods Syst. Des. 58(1-2): 5-41 (2021) - [c20]Yong Kiam Tan, André Platzer:
Switched Systems as Hybrid Programs. ADHS 2021: 247-252 - [c19]Katherine Cordwell
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. ITP 2021: 14:1-14:20 - [c18]Yong Kiam Tan
Deductive Stability Proofs for Ordinary Differential Equations. TACAS (2) 2021: 181-199 - [c17]Yong Kiam Tan
cake_lpr: Verified Propagation Redundancy Checking in CakeML. TACAS (2) 2021: 223-241 - [i12]Yong Kiam Tan, André Platzer:
Switched Systems as Hybrid Programs. CoRR abs/2101.06195 (2021) - [i11]Katherine Cordwell, Yong Kiam Tan, André Platzer:
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. CoRR abs/2102.03003 (2021) - [i10]Yong Kiam Tan, Stefan Mitsch, André Platzer:
Verifying Switched System Stability With Logic. CoRR abs/2111.01928 (2021) - 2020
- [j7]André Platzer
Differential Equation Invariance Axiomatization. J. ACM 67(1): 6:1-6:66 (2020) - [j6]Oskar Abrahamsson
Proof-Producing Synthesis of CakeML from Monadic HOL Functions. J. Autom. Reason. 64(7): 1287-1306 (2020) - [j5]Alejandro Gómez-Londoño
Do you have space for dessert? a verified space cost semantics for CakeML programs. Proc. ACM Program. Lang. 4(OOPSLA): 204:1-204:29 (2020) - [c16]Fabian Immler, Yong Kiam Tan:
The Poincaré-Bendixson theorem in Isabelle/HOL. CPP 2020: 338-352 - [i9]Yong Kiam Tan, André Platzer:
An Axiomatic Approach to Existence and Liveness for Differential Equations. CoRR abs/2004.14561 (2020) - [i8]Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer:
Pegasus: Sound Continuous Invariant Generation. CoRR abs/2005.09348 (2020) - [i7]Yong Kiam Tan, André Platzer:
Deductive Stability Proofs for Ordinary Differential Equations. CoRR abs/2010.13096 (2020)
2010 – 2019
- 2019
- [j4]Fabian Immler, Yong Kiam Tan:
The Poincaré-Bendixson Theorem. Arch. Formal Proofs 2019 (2019) - [j3]Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens
The verified CakeML compiler backend. J. Funct. Program. 29: e2 (2019) - [j2]Rose Bohrer
A Formal Safety Net for Waypoint-Following in Ground Robots. IEEE Robotics Autom. Lett. 4(3): 2910-2917 (2019) - [c15]Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan:
ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving. ARCH@CPSIoTWeek 2019: 141-161 - [c14]Andrew Sogokon
Pegasus: A Framework for Sound Continuous Invariant Generation. FM 2019: 138-157 - [c13]Yong Kiam Tan
An Axiomatic Approach to Liveness for Differential Equations. FM 2019: 371-388 - [c12]Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish
Verified compilation on a verified processor. PLDI 2019: 1041-1053 - [i6]Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, André Platzer:
A Formal Safety Net for Waypoint Following in Ground Robots. CoRR abs/1903.05073 (2019) - [i5]Yong Kiam Tan, André Platzer:
An Axiomatic Approach to Liveness for Differential Equations. CoRR abs/1904.07984 (2019) - [i4]André Platzer, Yong Kiam Tan:
Differential Equation Invariance Axiomatization. CoRR abs/1905.13429 (2019) - 2018
- [c11]Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan:
ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving. ARCH@ADHS 2018: 110-127 - [c10]Son Ho, Oskar Abrahamsson
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. IJCAR 2018: 646-662 - [c9]Andrew Sogokon
Vector Barrier Certificates and Comparison Systems. FM 2018: 418-437 - [c8]André Platzer
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. LICS 2018: 819-828 - [c7]Rose Bohrer
VeriPhy: verified controller executables from verified cyber-physical system models. PLDI 2018: 617-630 - [i3]André Platzer, Yong Kiam Tan:
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. CoRR abs/1802.01226 (2018) - 2017
- [j1]Scott Owens, Michael Norrish
Verifying efficient function calls in CakeML. Proc. ACM Program. Lang. 1(ICFP): 18:1-18:27 (2017) - [c6]Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar:
Verified compilation of CakeML to multiple machine-code targets. CPP 2017: 125-137 - 2016
- [c5]Scott Owens
Functional Big-Step Semantics. ESOP 2016: 589-615 - [c4]Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens
A new verified compiler backend for CakeML. ICFP 2016: 60-73 - [c3]Yong Kiam Tan, Xinxing Xu, Yong Liu:
Improved Recurrent Neural Networks for Session-based Recommendations. DLRS@RecSys 2016: 17-22 - [i2]Zhenzhou Wu, Sunil Sivadas, Yong Kiam Tan, Bin Ma, Rick Siow Mong Goh:
Multi-Modal Hybrid Deep Neural Network for Speech Enhancement. CoRR abs/1606.04750 (2016) - [i1]Yong Kiam Tan, Xinxing Xu, Yong Liu:
Improved Recurrent Neural Networks for Session-based Recommendations. CoRR abs/1606.08117 (2016) - 2015
- [c2]Yong Kiam Tan, Scott Owens
A verified type system for CakeML. IFL 2015: 7:1-7:12 - 2014
- [c1]Rubing Duan, Rick Siow Mong Goh, Feng Yang
Towards building and evaluating a personalized location-based recommender system. IEEE BigData 2014: 43-48
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-10 20:51 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: