| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Sat, 12 Jul 2025 03:38:35 GMT
access-control-allow-origin: *
etag: W/"6871d8bb-7045"
expires: Sun, 28 Dec 2025 19:19:38 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: AF80:15317B:7F12AA:8E7E99:69518071
accept-ranges: bytes
age: 0
date: Sun, 28 Dec 2025 19:09:38 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210068-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1766948978.156747,VS0,VE205
vary: Accept-Encoding
x-fastly-request-id: 63fda8b83443788992fdafa61ce1b0d7e1a6bc6c
content-length: 8046
Soonho Kong | Amazon Web Services
Soonho Kong
I’m a Principal Applied Scientist for Amazon Web Services working within the Neuro-Symbolic AI Lab. My research focuses on designing and implementing AI systems with formal reasoning capabilities, particularly combining LLMs with interactive and automated theorem proving techniques. My work helps improve Amazon Nova models with advanced reasoning capabilities. I earned my PhD from Carnegie Mellon University under Prof. Edmund Clarke, focusing on delta-decision procedures.
I received the ACM SIGPLAN Programming Languages Software Award and the CADE Skolem Award for my contributions to the Lean theorem prover.
email address
github.com/soonhokong
cv.pdf
Software
- Lean: Contributor (2013 – ) (more info)
- dReal4: Maintainer (2013 – )
- Drake: Platform-reviewer / Contributor (2016 – 2021)
Publications
- Solving string constraints with concatenation using SAT.
Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, and Dirk Nowotka.
In FMCAD 2024, 2024.
[ bib | http ] - Solving String Constraints Using SAT.
Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Rupak Majumdar, and Dirk Nowotka.
In Computer Aided Verification, pages 187--208, Cham, 2023. Springer Nature Switzerland.
[ bib | http ] - Certified Perception for Autonomous Cars.
U. Guajardo, A. Bryan, N. Arechiga, S. Campos, J. Chow, D. Jackson, S. Kong, G. Litt, and J. Pollock.
6th Workshop On Monitoring And Testing Of Cyber-Physical Systems, 2021.
[ bib | http ] - Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems.
Sicun Gao, James Kapinski, Jyotirmoy Deshmukh, Nima Roohi, Armando Solar-Lezama, Nikos Arechiga, and Soonho Kong.
In Computer Aided Verification, pages 137--154, Cham, 2019. Springer International Publishing.
[ bib | DOI | .pdf ] - Evaluating Branching Heuristics in Interval Constraint Propagation for Satisfiability.
Calvin Huang, Soonho Kong, Sicun Gao, and Damien Zufferey.
In Numerical Software Verification, pages 85--100, Cham, 2019. Springer International Publishing.
[ bib | DOI | http ] - Certified Control for Self-Driving Cars.
Daniel Jackson, Jonathan DeCastro, Soonho Kong, Dimitrios Koutentakis, Angela Feng Ping Leong, Armando Solar-Lezama, Mike Wang, and Xin Zhang.
In DARS 2019: 4th Workshop On The Design And Analysis Of Robust Systems, 2019.
[ bib | .pdf ] - Better AI through Logical Scaffolding.
Nikos Arechiga, Jonathan DeCastro, Soonho Kong, and Karen Leung.
In FoMLAS 2019: 2nd Workshop on Formal Methods for ML-Enabled Autonomous Systems, 2019.
[ bib | http ] - Delta-Decision Procedures for Exists-Forall Problems over the Reals.
Soonho Kong, Armando Solar-Lezama, and Sicun Gao.
In Computer Aided Verification, CAV'18, pages 219--235, Cham, 2018. Springer International Publishing.
[ bib | DOI | .pdf ] - SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems.
Kyungmin Bae, Peter Csaba Ölveczky, Soonho Kong, Sicun Gao, and Edmund M. Clarke.
In Hybrid Systems: Computation and Control, HSCC'16, pages 145--154, New York, NY, USA, 2016. ACM.
[ bib | DOI | http ] - A network-driven approach for genome-wide association mapping.
Seunghak Lee, Soonho Kong, and Eric P. Xing.
Bioinformatics, 32(12):i164--i173, 2016.
[ bib | DOI | http ] - Bifurcation Analysis of Cardiac Alternans Using delta-Decidability.
Md. Ariful Islam, Greg Byrne, Soonho Kong, Edmund M. Clarke, Rance Cleaveland, Flavio H. Fenton, Radu Grosu, Paul L. Jones, and Scott A. Smolka.
In Computational Methods in Systems Biology, CMSB'16, pages 132--146, Cham, 2016. Springer International Publishing.
[ bib | DOI ] - dReach: Delta-Reachability Analysis for Hybrid Systems.
Soonho Kong, Sicun Gao, Wei Chen, and Edmund Clarke.
In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'15, pages 200--205, New York, NY, USA, 2015. Springer-Verlag New York, Inc.
[ bib | DOI | http ] - Towards Personalized Prostate Cancer Therapy Using Delta-reachability Analysis.
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, and Edmund M. Clarke.
In Hybrid Systems: Computation and Control, HSCC'15, pages 227--232, New York, NY, USA, 2015. ACM.
[ bib | DOI | http ] - The Lean Theorem Prover (System Description).
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer.
In Automated Deduction, CADE'15, pages 378--388, Cham, 2015. Springer International Publishing.
[ bib | DOI ] - SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems.
Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao, and Edmund M. Clarke.
In Computational Methods in Systems Biology, CMSB'15, pages 15--27, Cham, 2015. Springer International Publishing.
[ bib | DOI ] - Parameter Synthesis for Cardiac Cell Hybrid Models Using δ-Decisions.
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, and Edmund M. Clarke.
In Computational Methods in Systems Biology, CMSB'14, pages 99--113, Cham, 2014. Springer International Publishing.
[ bib | DOI ] - Proof Generation from Delta-Decisions.
Sicun Gao, Soonho Kong, and Edmund M. Clarke.
In Symbolic and Numeric Algorithms for Scientific Computing, SYNASC'14, pages 156--163, 9 2014.
[ bib | DOI ] - Automatically inferring loop invariants via algorithmic learning.
Yungbum Jung, Soonho Kong, Cristina David, Bow-Yaw Wang, and Kwangkeun Yi.
Mathematical Structures in Computer Science, 25(4):892–915, 2015.
[ bib | DOI ] - Satisfiability modulo ODEs.
Sicun Gao, Soonho Kong, and Edmund M. Clarke.
In Formal Methods in Computer-Aided Design, FMCAD'13, pages 105--112, 2013.
[ bib | DOI ] - dReal: An SMT Solver for Nonlinear Theories over the Reals.
Sicun Gao, Soonho Kong, and Edmund M. Clarke.
In Automated Deduction, CADE'13, pages 208--214, Berlin, Heidelberg, 2013. Springer-Verlag.
[ bib | DOI | http ] - Compositional Sequentialization of Periodic Programs.
Sagar Chaki, Arie Gurfinkel, Soonho Kong, and Ofer Strichman.
In Verification, Model Checking, and Abstract Interpretation, VMCAI'13, pages 536--554, New York, NY, USA, 2013. Springer-Verlag New York, Inc.
[ bib | DOI | http ] - Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates.
Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, and Kwangkeun Yi.
In Asian Conference on Programming Languages and Systems, APLAS'10, pages 328--343, Berlin, Heidelberg, 2010. Springer-Verlag.
[ bib | DOI | http ] - Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction.
Yungbum Jung, Soonho Kong, Bow-Yaw Wang, and Kwangkeun Yi.
In Verification, Model Checking, and Abstract Interpretation, VMCAI'10, pages 180--196, Berlin, Heidelberg, 2010. Springer-Verlag.
[ bib | DOI | http ] - Abstract Parsing for Two-staged Languages with Concatenation.
Soonho Kong, Wontae Choi, and Kwangkeun Yi.
In Generative Programming and Component Engineering, GPCE'09, pages 109--116, New York, NY, USA, 2009. ACM.
[ bib | DOI | http ] - PCC Framework for Program-Generators.
Soonho Kong, Wontae Choi, and Kwangkeun Yi.
In Workshop on Proof-Carrying Code and Software Certification, 2009.
[ bib | .pdf ] - Automated Testing of Environment-Dependent Programs - A Case Study of Modeling the File System for Pex.
Soonho Kong, Nikolai Tillmann, and Jonathan de Halleux.
In Information Technology: New Generations, ITNG'09, pages 758--762, 4 2009.
[ bib | DOI ]
Patents
- Systems and methods for automatically generating solver code for nonlinear model predictive control solvers.
Sarah Koehler, Soonho Kong, Frank Permenter, Kevin Zaseck, and Avinash Balachandran
United States Patent #12208809. January 2025.
[ bib | .pdf ] - Wearable exoskeleton.
Jonathan DeCastro, Soon Ho Kong, Nikos Gonzalez Arechiga, Frank Permenter, and Dennis Park
United States Patent #11918535. March 2024.
[ bib | .pdf ] - Actively adapting to driving environments based on human interactions.
Soon Ho Kong, Jonathan DeCastro, Nikos Gonzalez Arechiga, and Frank Permenter
United States Patent #11918535. October 2023.
[ bib | .pdf ] - Certified control for self-driving cars.
Daniel Jackson, Jonathan Decastro, Soon Ho Kong, Nikos Arechiga Gonzalez, Dimitrios Koutentakis, Feng Ping Angela Leong, Mike Meichang Wang, and Xin Zhang
United States Patent #11745732. September 2023.
[ bib | .pdf ] - Predictive impairment monitor system and method.
Nikos Gonzalez Arechiga, Soon Ho Kong, Jonathan DeCastro, Frank Permenter, and Dennis Park
United States Patent #11518408. December 2022.
[ bib | .pdf ] - Predictive parking due to weather.
Nikos Gonzalez Arechiga, Soon Ho Kong, Jonathan DeCastro, Frank Permenter, and Dennis Park
United States Patent #11479239. October 2022.
[ bib | .pdf ] - Simulation-based Technique to Synthesize Controllers that Satisfy Signal Temporal Logic Specifications.
Nikos Arechiga, Karen Y. Leung, Soon Ho Kong, Jonathan Decastro, and Frank Permenter
United States Patent #11256611. February 2022.
[ bib | .pdf ] - System and Method for Detecting Errors and Improving Reliability of Perception Systems Using Logical Scaffolds.
Nikos Arechiga, Soonho Kong, Jonathan DeCastro, Sagar Behere, and Dennis Park
United States Patent #11157756. October 2021.
[ bib | .pdf ] - Actively Adapting To Driving Environments Based On Human Interactions.
Soonho Kong, Jonathan DeCastro, Nikos Arechiga, and Frank Permenter
United States Patent #11072342. July 2021.
[ bib | .pdf ] - Systems And Methods For Improving Situational Awareness Of A User.
Jonathan DeCastro, Frank Permenter, Soonho Kong, and Nikos Arechiga
United States Patent #10621858. April 2020.
[ bib | .pdf ]
Talks
- 2025/07/11 Lean into Verifiable Intelligence @LeanQC (Quantum Computing), University of Michigan, Ann Arbor, MI.
- 2025/07/03 Lean into Verifiable Intelligence @UpStage AI, Seoul, South Korea.
- 2025/06/23 Lean into Verifiable Intelligence @Seoul National University, Seoul, South Korea.
- 2025/06/20 Lean into the Future – Self Verification, the Key to AI @Samsung Research, Seoul, South Korea.
- 2025/06/20 Lean into the Future – Self Verification, the Key to AI @LG AI Research, Seoul, South Korea.
- 2025/06/19 AI+Lean: Neurosymbolic AI @PLDI 2025, Seoul, South Korea.
- 2025/06/02 AI Challenges for Academia – An Industry Perspective @TILOS Industry Day 2025, UCSD, San Diego, CA.
- 2024/12/19 Lean into the Future – New Horizons in Mathematics, Programming, and AI @Seoul National University, Seoul, Korea.
- 2024/12/17 Lean into the Future – New Horizons in Mathematics, Programming, and AI @AI for Mathematics Workshop on Formalization, KIAS, Seoul, Korea.
- 2018/07/17 Delta-Decision Procedures for Exists-Forall Problems over the Reals @CAV 2018, Oxford, UK. [Slides]
- 2018/06/23 ℝeal Problems on the Road @FoMA 2018, CMU, Pittsburgh, PA. [Slides]
- 2018/04/25 Drake: Dynamical Systems and Automotive Components @MIT [Slides]
- 2016/04/28 Efficient Delta-decision Procedure @CMU [Slides]
- 2016/04/06 Automated Reasoning over the Reals @Toyota Research Institute [Slides]
- 2016/03/16 Delta-Reachability Analysis for Hybrid Systems @Microsoft Research Redmond [Slides]
- 2016/01/07 Delta-Reachability Analysis for Hybrid Systems @Microsoft Research Cambridge, UK [Slides]
- 2015/05/18 Delta-Reachability Analysis for Hybrid Systems @CMU SCS Speakers Club Talk [Slides]
- 2015/04/14 dReach: Delta-Reachability Analysis for Hybrid Systems @TACAS 2015, London, UK [Slides]
- 2013/06/12 dReal: An SMT solver for nonlinear theories of the reals @CADE 2013, Lake Placid, New York, U.S. [Slides]
- 2012/09/21 Compositional Sequentialization of Periodic Programs @Programming Research Lab, Seoul National University [Slides]
- 2012/08/09 Verifying Concurrent Turing Machines @SAS Unit Meeting, CMU SEI [Slides]
- 2011/11/09 Abstract Interpretation @CMU 15–414, Class Lecture [Slides]
- 2011/10/10 Model Checking @CMU 15–414, Class Lecture [Slides]
- 2011/03/23 Basic Concepts of Abstract Interpretation @CMU 15–817, Class Lecture [Slides]
- 2011/01/26 Data Flow Analysis @CMU 15–817, Class Lecture [Slides]
- 2010/01/18 Deriving Invariants in Propositional Logic by Algorithmic Learning, Decision Procedures, and Predicate Abstraction @VMCAI 2010, Madrid, Spain [Slides/photo]
- 2009/12/14 Deriving Invariants in Propositional Logic by Algorithmic Learning, Decision Procedures, and Predicate Abstraction @APLAS 2009, Seoul, Korea (Poster Session) [poster/photo]
- 2009/08/15 PCC Framework for Program Generators @PCC 2009, Los Angeles, U.S.A [Slides]
Professional Activities
Program committee member
- MEMOCODE 2021: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design
- ADHS 2021: 7th IFAC Conference on Analysis and Design of Hybrid Systems: Repeatability Evaluation
- HSCC 2021: 24rd International Conference on Hybrid Systems: Computation and Control: Repeatability Evaluation
- MT-CPS 2021: 6th Workshop on Monitoring and Testing of Cyber-physical Systems
- HSCC 2020: 23rd International Conference on Hybrid Systems: Computation and Control: Repeatability Evaluation
- MEMOCODE 2020: 18th ACM-IEEE International Conference on Formal Methods and Models for System Design
- SpringSim 2020: Spring Simulation Conference 2020
- MEMOCODE 2019: 17th ACM-IEEE International Conference on Formal Methods and Models for System Design
- HSCC 2019: 22nd International Conference on Hybrid Systems: Computation and Control: Repeatability Evaluation
- NSV 2019: 12th International Workshop on Numerical Software Verification 2019
- DARS 2019: 4th Workshop on the Design and Analysis of Robust Systems
- WSC 2018: Winter Simulation Conference 2018 (Cyber-Physical Systems track)
- DARS 2018: Third Workshop on Design and Analysis of Robust Systems
External reviewer
IEEE IV 2021, IEEE IV 2020, POPL 2020, ATVA 2015, ASE 2014, SAS 2013, FoSSaCS 2013, POPL 2013, APLAS 2012, SAS 2012, GPCE 2010, SPLASH 2010, CAV 2010, VMCAI 2010, SAS 2009, DEFECTS 2009, APLAS 2007
"We can only see a short distance ahead, but we can see plenty there that needs to be done."