Soonho Kong

Research scientist at Toyota Research Institute
Research interests: automated reasoning and its applications toward robust cyber-physical systems.

email soonho.kong@tri.global
github github.com/soonho-tri
cv cv.pdf
location Cambridge, MA

Software

Publications

[Google Scholar/DBLP]

 
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 ]

Talks

Professional Activities

Program committee member

External reviewer

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."