publications

[Google Scholar/DBLP]

2016

  • SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems Kyungmin Bae, Peter Olveczky, Soonho Kong, and Sicun Gao. HSCC 2016: Hybrid Systems Computation and Control, April 12-14, 2016, Vienna, Austria. [doi]

  • A Network-driven Approach for Genome-wide Association Mapping Seunghak Lee, Soonho Kong, and Eric Xing. ISMB 2016: International Conference on Intelligent Systems for Molecular Biology, July 8-12, 2016, in Orlando, Florida . [PDF]

  • Bifurcation Analysis of Cardiac Alternans using delta-Decidability Md. Ariful Islam, Greg Byrne, Soonho Kong, Edmund Clarke, Rance Cleaveland, Radu Grosu, and Scott Smolka. CMSB 2016: Computational Methods in Systems Biology, Cambridge, UK, Sep 21 - 23, 2016.

  • Elaboration in dependent type theory Leonardo de Moura, Jeremy Avigad, Soonho Kong, and Cody Roux. Draft. [arXiv]

2015

  • dReach: Delta-Reachability Analysis for Hybrid Systems Soonho Kong, Sicun Gao, Wei Chen, and Edmund Clarke. TACAS 2015: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, London, UK, April 11 - 18, 2015. [PDF/Slides/Tool]

  • Towards Personalized Prostate Cancer Therapy Using Delta-Reachability Analysis Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, and Edmund Clarke. HSCC 2015: Hybrid Systems Computation and Control, Seattle, USA, April 14 - 16, 2015. [PDF]

  • The Lean theorem prover (system description) Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, Aug 1 - 8, 2015. [PDF/Tool]

  • SReach: A Probabilistic Bounded delta-Reachability Analyzer for Stochastic Hybrid Systems Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao and Edmund Clarke. CMSB 2015: Computational Methods in Systems Biology, Nantes, France, Sep 16 - 18, 2015. [PDF/Tool]

  • Theorem Proving in Lean Jeremy Avigad, Leonardo de Moura, Soonho Kong. [PDF/HTML]

2014

  • Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, and Edmund Clarke. CMSB 2014: Computational Methods in Systems Biology, Manchester, UK, November 17 - 19, 2014. [arXiv]

  • Proof Generation from Delta-Decisions Sicun Gao, Soonho Kong, and Edmund Clarke. SYNASC 2014: International Conference on Symbolic and Numerical Algorithms for Scientific Computing, Timisoara, Romania, September 22 - 25, 2014. [arXiv]

  • Automatically Inferring Loop Invariants via Algorithmic Learning. Yungbum Jung, Soonho Kong, Cristina David, Bow-Yaw Wang, and Kwangkeun Yi. Mathematical Structures in Computer Science, 2014. [DOI]

2013

  • Satisfiability Modulo ODEs Sicun Gao, Soonho Kong, and Edmund Clarke. FMCAD 2013: Formal Methods in Computer-Aided Design, Portland, Oregon, October 20 - 23, 2013. [PDF]

  • dReal: An SMT Solver for Nonlinear Theories of Reals (Tool Paper) Sicun Gao, Soonho Kong, and Edmund Clarke. CADE 2013: 24th International Conference on Automated Deduction , Lake Placid, New York, June 9 - 14, 2013. [PDF/Slides/Tool]

  • Compositional Sequentialization of Periodic Programs. Sagar Chaki, Arie Gurfinkel, Soonho Kong and Ofer Strichman. VMCAI 2013: 14th International Conference on Verification, Model Checking, and Abstract Interpretation, Rome, Jan 20 - 22, 2013. [PDF/BibTeX/Slides/Tool]

2010

  • Automatically Inferring Quantified Invariants via Algorithmic Learning from Simple Templates. Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, Kwangkeun Yi. APLAS 2010 The 8th ASIAN Symposium on Programming Languages and Systems, Nov 28 - Dec 1, 2010. [PDF/BibTeX/Slides(courtesy of Yungbum Jung)]

  • Deriving Invariants in Propositional Logic by Algorithmic Learning, Decision Procedures, and Predicate Abstraction. Yungbum Jung, Soonho Kong, Bow-Yaw Wang, Kwangkeun Yi. VMCAI 2010: The 11th International Conference on Verification, Model Checking, and Abstract Interpretation, Madrid, Jan 17-19, 2010. [PDF/BibTeX/Slides]

2009

  • Abstract Parsing for Two-staged Languages with Concatenation. Soonho Kong, Wontae Choi, Kwangkeun Yi. GPCE 2009: The 8th International Conference on Generative Programming and Component Engineering, Denver, Oct 4-5, 2009. [PDF/BibTeX/Slides]

  • PCC Framework for Program Generators. Soonho Kong, Wontae Choi, Kwangkeun Yi. PCC 2009: The 3rd International Workshop on Proof-Carrying Code and Software Certification, Los Angeles, Aug 15, 2009. [PDF/BibTeX/Slides]

  • Automated Testing of Environment-Dependent Programs - A Case Study of Modeling the File System for Pex. Soonho Kong, Nikolai Tillmann, Jonathan de Halleux. ITNG 2009: The 6th International Conference on Information Technology: New Generations, Las Vegas, Apr 27-29, 2009. [PDF/BibTeX]

2007

  • Sparrow: The Source Code Analyzer. Hakjoo Oh, Yungbum Jung, Minsik Jin, Deokhwan Kim, Yikwon Hwang, Daejun Park, Heejong Lee, Soonho Kong, Kwangkeun Yi. KIISE(Korean Institute of Information Scientists and Engineers) Conference 2007, 34(1C):500–504, KIISE, 2007. [PDF (in Korean)]