SK
Soonho Kong
cs.LOcs.AIcs.LGcs.SEcs.PLcs.SYeess.SYcs.CLq-bio.QMcs.CC
On Valency
published · living versionsW_etmeccs6·v1 · currentpublished
Scaling Lean Theorem Proving for Real-World Code Verification
with Debargha Ganguly, Divya Raghunathan, Dejan Jovanović, Vikash Singh +4
1 version
Preprints & journals
22 papers in the corpus · 2013–2026TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science2609.35606v1 · Chutong Yang, Xiyuan Zhang, Yu Huang et al.2026 · 0 citationsarXiv
SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization2608.29270v3 · Hojae Han, Jongyoon Kim, Sanghyeok Park et al.2026 · 0 citationsThe 2026 Conference on Empirical Methods in Natural Language Processing
Vero: Can AI Agents Build Formally Verified Software Repositories?2608.13522v1 · Zhe Ye, Hantao Lou, Yuechun Sun et al.2026 · 0 citationsarXiv
Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search2605.20244v2 · Jialin Lu, Soonho Kong, Rodrigo Stehling et al.2026 · 0 citationsarXiv
Teaching LLMs Program Semantics via Symbolic Execution Traces2605.06184v1 · Jonas Bayer, Stefan Zetzsche, Olivier Bouissou et al.2026 · 0 citationsarXiv
Intent-aligned Formal Specification Synthesis via Traceable Refinement2604.10392v1 · Zhe Ye, Aidan Z.H. Yang, Huangyuan Su et al.2026 · 0 citationsarXiv
s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs2603.14628v2 · Balaji Rao, John Harrison, Soonho Kong et al.2026 · 0 citationsarXiv
Learning Adaptive LLM Decoding2603.09065v2 · Chloe H. Su, Zhe Ye, Samuel Tenka et al.2026 · 0 citationsarXiv
ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis2512.10173v2 · Mantas Baksys, Stefan Zetzsche, Olivier Bouissou et al.2025 · 1 citationarXiv
Certified Control: An Architecture for Verifiable Safety of Autonomous Vehicles2104.06178v1 · Daniel Jackson, Valerie Richmond, Mike Wang et al.2021 · 6 citationsarXiv
Better AI through Logical Scaffolding1909.06965v1 · Nikos Arechiga, Jonathan DeCastro, Soonho Kong et al.2019 · 1 citationarXiv
Delta-Decision Procedures for Exists-Forall Problems over the Reals1807.08137v1 · Soonho Kong, Armando Solar-Lezama, Sicun Gao2018 · 18 citationsarXiv
REAS: Combining Numerical Optimization with SAT Solving1802.04408v1 · Jeevana Priya Inala, Sicun Gao, Soonho Kong et al.2018 · 7 citationsarXiv
A network-driven approach for genome-wide association mapping.27307613 · Lee, Seunghak, Kong, Soonho, Xing, Eric P2017 · 11 citationsBioinformatics (Oxford, England). 2016;32(12):i164-i173
Elaboration in Dependent Type Theory1505.04324v2 · Leonardo de Moura, Jeremy Avigad, Soonho Kong et al.2015 · 10 citationsarXiv
Towards Personalized Prostate Cancer Therapy Using Delta-Reachability Analysis1410.7346v3 · Bing Liu, Soonho Kong, Sicun Gao et al.2014 · 13 citationsarXiv
Proof Generation from Delta-Decisions1409.6414v1 · Sicun Gao, Soonho Kong, Edmund Clarke2014 · 8 citationsarXiv
Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions1407.1524v3 · Bing Liu, Soonho Kong, Sicun Gao et al.2014 · 7 citationsarXiv
SReach: A Bounded Model Checker for Stochastic Hybrid Systems1404.7206v2 · Qinsi Wang, Paolo Zuliani, Soonho Kong et al.2014 · 5 citationsarXiv
Revisiting the Complexity of Stability of Continuous and Hybrid Systems1404.7169v4 · Sicun Gao, Soonho Kong, Edmund Clarke2014 · 0 citationsarXiv
Delta-Complete Analysis for Bounded Reachability of Hybrid Systems1404.7171v1 · Sicun Gao, Soonho Kong, Wei Chen et al.2014 · 31 citationsarXiv
Satisfiability Modulo ODEs1310.8278v1 · Sicun Gao, Soonho Kong, Edmund Clarke2013 · 72 citationsarXiv
Career total: 49 works. 22 are in this corpus.
Profile built from the corpus for this byline.
Author records are still filling in while the Hub is in alpha. If this is your page, you'll be able to claim it soon. Spot a mistake? Tell us.