publications.bib

@inproceedings{Lotz2024,
  author = {Kevin Lotz and Amit Goel and Bruno Dutertre and Benjamin Kiesl-Reiter and Soonho Kong and Dirk Nowotka},
  title = {Solving string constraints with concatenation using SAT},
  year = {2024},
  url = {https://www.amazon.science/publications/solving-string-constraints-with-concatenation-using-sat},
  booktitle = {FMCAD 2024}
}

@inproceedings{10.1007/978-3-031-37703-7_9,
  abstract = {String solvers are automated-reasoning tools that can solve combinatorial problems over formal languages. They typically operate on restricted first-order logic formulas that include operations such as string concatenation, substring relationship, and regular expression matching. String solving thus amounts to deciding the satisfiability of such formulas. While there exists a variety of different string solvers, many string problems cannot be solved efficiently by any of them. We present a new approach to string solving that encodes input problems into propositional logic and leverages incremental SAT solving. We evaluate our approach on a broad set of benchmarks. On the logical fragment that our tool supports, it is competitive with state-of-the-art solvers. Our experiments also demonstrate that an eager SAT-based approach complements existing approaches to string solving in this specific fragment.},
  address = {Cham},
  author = {Lotz, Kevin and Goel, Amit and Dutertre, Bruno and Kiesl-Reiter, Benjamin and Kong, Soonho and Majumdar, Rupak and Nowotka, Dirk},
  booktitle = {Computer Aided Verification},
  editor = {Enea, Constantin and Lal, Akash},
  isbn = {978-3-031-37703-7},
  pages = {187--208},
  publisher = {Springer Nature Switzerland},
  title = {Solving String Constraints Using SAT},
  url = {https://www.amazon.science/publications/solving-string-constraints-using-sat},
  year = 2023
}

@article{osti_10272149,
  place = {Country unknown/Code not available},
  title = {Certified Perception for Autonomous Cars},
  url = {https://par.nsf.gov/servlets/purl/10272149},
  abstractnote = {We present a method for establishing confidence in the decisions of an autonomous car which accounts for errors not only in control but also in perception. The key idea is that the controller generates a certificate, which is a kind its proposed action is safe. of proof that its interpretation of the scene is accurate and its proposed action is safe. Checking the certificate is faster and simpler than generating it, which allows for a monitor that comprises a much smaller trusted base than the system as a whole. Simulation experiments suggest that the approach is practical.},
  journal = {6th Workshop On Monitoring And Testing Of Cyber-Physical Systems},
  author = {Guajardo, U. and Bryan, A. and Arechiga, N. and Campos, S. and Chow, J. and Jackson, D. and Kong, S. and Litt, G. and Pollock, J.},
  year = 2021
}

@inproceedings{10.1007/978-3-030-25543-5_9,
  author = {Gao, Sicun
and Kapinski, James
and Deshmukh, Jyotirmoy
and Roohi, Nima
and Solar-Lezama, Armando
and Arechiga, Nikos
and Kong, Soonho},
  editor = {Dillig, Isil
and Tasiran, Serdar},
  title = {Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems},
  booktitle = {Computer Aided Verification},
  year = 2019,
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {137--154},
  abstract = {We formulate numerically-robust inductive proof rules for unbounded stability and safety properties of continuous dynamical systems. These induction rules robustify standard notions of Lyapunov functions and barrier certificates so that they can tolerate small numerical errors. In this way, numerically-driven decision procedures can establish a sound and relative-complete proof system for unbounded properties of very general nonlinear systems. We demonstrate the effectiveness of the proposed rules for rigorously verifying unbounded properties of various nonlinear systems, including a challenging powertrain control model.},
  isbn = {978-3-030-25543-5},
  doi = {10.1007/978-3-030-25543-5_9},
  url = {https://link.springer.com/content/pdf/10.1007/978-3-030-25543-5_9.pdf}
}

@inproceedings{10.1007/978-3-030-28423-7_6,
  author = {Huang, Calvin
and Kong, Soonho
and Gao, Sicun
and Zufferey, Damien},
  editor = {Zamani, Majid
and Zufferey, Damien},
  title = {Evaluating Branching Heuristics in Interval Constraint Propagation for Satisfiability},
  booktitle = {Numerical Software Verification},
  year = 2019,
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {85--100},
  abstract = {Interval Constraint Propagation (ICP) is a powerful method for solving general nonlinear constraints over real numbers. ICP uses interval arithmetic to prune the space of potential solutions and, when the constraint propagation fails, divides the space into smaller regions and continues recursively. The original goal is to find paving boxes of all solutions to a problem. Already when the whole domain needs to be considered, branching methods do matter much. However, recent applications of ICP in decision procedures over the reals need only a single solution. Consequently, variable ordering in branching operations becomes even more important.},
  isbn = {978-3-030-28423-7},
  doi = {10.1007/978-3-030-28423-7_6},
  url = {https://link.springer.com/chapter/10.1007/978-3-030-28423-7_6}
}

@inproceedings{dars2019,
  author = {Jackson, Daniel and DeCastro, Jonathan and Kong, Soonho and Koutentakis, Dimitrios and Leong, Angela Feng Ping and Solar-Lezama, Armando and Wang, Mike and Zhang, Xin},
  title = {Certified Control for Self-Driving Cars},
  booktitle = {DARS 2019: 4th Workshop On The Design And Analysis Of Robust Systems},
  year = 2019,
  url = {https://soonhokong.github.io/pubs/2019_DARS_Certified_Control_for_Self-Driving_Cars.pdf}
}

@inproceedings{fomlas2019,
  title = {Better AI through Logical Scaffolding},
  author = {Nikos Arechiga and Jonathan DeCastro and Soonho Kong and Karen Leung},
  year = 2019,
  booktitle = {FoMLAS 2019: 2nd Workshop on Formal Methods for ML-Enabled Autonomous Systems},
  url = {https://arxiv.org/pdf/1909.06965}
}

@inproceedings{10.1007/978-3-319-96142-2_15,
  author = {Kong, Soonho
and Solar-Lezama, Armando
and Gao, Sicun},
  editor = {Chockler, Hana
and Weissenbacher, Georg},
  title = {Delta-Decision Procedures for Exists-Forall Problems over the Reals},
  booktitle = {Computer Aided Verification},
  series = {CAV'18},
  year = 2018,
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {219--235},
  isbn = {978-3-319-96142-2},
  doi = {10.1007/978-3-319-96142-2_15},
  url = {https://link.springer.com/content/pdf/10.1007/978-3-319-96142-2_15.pdf}
}

@inproceedings{Bae:2016:SAV:2883817.2883849,
  author = {Bae, Kyungmin and \"{O}lveczky, Peter Csaba and Kong, Soonho and Gao, Sicun and Clarke, Edmund M.},
  title = {{SMT}-Based Analysis of Virtually Synchronous Distributed Hybrid Systems},
  booktitle = {Hybrid Systems: Computation and Control},
  series = {HSCC'16},
  year = 2016,
  isbn = {978-1-4503-3955-1},
  location = {Vienna, Austria},
  pages = {145--154},
  numpages = 10,
  url = {http://doi.acm.org/10.1145/2883817.2883849},
  doi = {10.1145/2883817.2883849},
  acmid = 2883849,
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {distributed hybrid systems, pals, smt, synchronizers}
}

@article{doi:10.1093/bioinformatics/btw270,
  author = {Lee, Seunghak and Kong, Soonho and Xing, Eric P.},
  title = {A network-driven approach for genome-wide association mapping},
  journal = {Bioinformatics},
  volume = 32,
  number = 12,
  pages = {i164-i173},
  year = 2016,
  doi = {10.1093/bioinformatics/btw270},
  url = {http://dx.doi.org/10.1093/bioinformatics/btw270}
}

@inproceedings{10.1007/978-3-319-45177-0_9,
  author = {Islam, Md. Ariful
and Byrne, Greg
and Kong, Soonho
and Clarke, Edmund M.
and Cleaveland, Rance
and Fenton, Flavio H.
and Grosu, Radu
and Jones, Paul L.
and Smolka, Scott A.},
  editor = {Bartocci, Ezio
and Lio, Pietro
and Paoletti, Nicola},
  title = {Bifurcation Analysis of Cardiac Alternans Using delta-Decidability},
  booktitle = {Computational Methods in Systems Biology},
  series = {CMSB'16},
  year = 2016,
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {132--146},
  isbn = {978-3-319-45177-0},
  doi = {10.1007/978-3-319-45177-0_9}
}

@inproceedings{Kong:2015:D9A:2945565.2945606,
  author = {Kong, Soonho and Gao, Sicun and Chen, Wei and Clarke, Edmund},
  title = {{dReach}: Delta-Reachability Analysis for Hybrid Systems},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
  series = {TACAS'15},
  year = 2015,
  isbn = {978-3-662-46680-3},
  pages = {200--205},
  numpages = 6,
  url = {https://doi.org/10.1007/978-3-662-46681-0_15},
  doi = {10.1007/978-3-662-46681-0_15},
  acmid = 2945606,
  publisher = {Springer-Verlag New York, Inc.},
  address = {New York, NY, USA}
}

@inproceedings{Liu:2015:TPP:2728606.2728634,
  author = {Liu, Bing and Kong, Soonho and Gao, Sicun and Zuliani, Paolo and Clarke, Edmund M.},
  title = {Towards Personalized Prostate Cancer Therapy Using Delta-reachability Analysis},
  booktitle = {Hybrid Systems: Computation and Control},
  series = {HSCC'15},
  year = 2015,
  isbn = {978-1-4503-3433-4},
  location = {Seattle, Washington},
  pages = {227--232},
  numpages = 6,
  url = {http://doi.acm.org/10.1145/2728606.2728634},
  doi = {10.1145/2728606.2728634},
  acmid = 2728634,
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {delta-reachability, hybrid systems, personalized therapy, prostate cancer, systems biology}
}

@inproceedings{10.1007/978-3-319-21401-6_26,
  author = {de Moura, Leonardo
and Kong, Soonho
and Avigad, Jeremy
and van Doorn, Floris
and von Raumer, Jakob},
  editor = {Felty, Amy P.
and Middeldorp, Aart},
  title = {The Lean Theorem Prover (System Description)},
  booktitle = {Automated Deduction},
  series = {CADE'15},
  year = 2015,
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {378--388},
  isbn = {978-3-319-21401-6},
  doi = {10.1007/978-3-319-21401-6_26}
}

@inproceedings{10.1007/978-3-319-23401-4_3,
  author = {Wang, Qinsi
and Zuliani, Paolo
and Kong, Soonho
and Gao, Sicun
and Clarke, Edmund M.},
  editor = {Roux, Olivier
and Bourdon, J{\'e}r{\'e}mie},
  title = {{SReach}: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems},
  booktitle = {Computational Methods in Systems Biology},
  series = {CMSB'15},
  year = 2015,
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {15--27},
  isbn = {978-3-319-23401-4},
  doi = {10.1007/978-3-319-23401-4_3}
}

@inproceedings{10.1007/978-3-319-12982-2_8,
  author = {Liu, Bing
and Kong, Soonho
and Gao, Sicun
and Zuliani, Paolo
and Clarke, Edmund M.},
  editor = {Mendes, Pedro
and Dada, Joseph O.
and Smallbone, Kieran},
  title = {Parameter Synthesis for Cardiac Cell Hybrid Models Using $\delta$-Decisions},
  booktitle = {Computational Methods in Systems Biology},
  series = {CMSB'14},
  year = 2014,
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {99--113},
  isbn = {978-3-319-12982-2},
  doi = {10.1007/978-3-319-12982-2_8}
}

@inproceedings{7034679,
  author = {Sicun Gao and Soonho Kong and Edmund M. Clarke},
  booktitle = {Symbolic and Numeric Algorithms for Scientific Computing},
  series = {SYNASC'14},
  title = {Proof Generation from Delta-Decisions},
  year = 2014,
  pages = {156-163},
  keywords = {calculus;computability;theorem proving;Kepler conjecture;automated theorem proving;constraint solving;delta-complete decision procedure;first-order calculus;logical proof;proof generation;proof-checking algorithm;unsatisfiability;Abstracts;Algorithm design and analysis;Calculus;Iterative closest point algorithm;Polynomials;Reliability;Transforms},
  doi = {10.1109/SYNASC.2014.29},
  month = {9}
}

@article{jung_kong_david_wang_yi_2015,
  title = {Automatically inferring loop invariants via algorithmic learning},
  volume = 25,
  doi = {10.1017/S0960129513000078},
  number = 4,
  journal = {Mathematical Structures in Computer Science},
  publisher = {Cambridge University Press},
  author = {Jung, Yungbum and Kong, Soonho and David, Cristina and Wang, Bow-Yaw and Yi, Kwangkeun},
  year = 2015,
  pages = {892–915}
}

@inproceedings{Gao2013SatisfiabilityMO,
  title = {Satisfiability modulo {ODEs}},
  author = {Sicun Gao and Soonho Kong and Edmund M. Clarke},
  booktitle = {Formal Methods in Computer-Aided Design},
  series = {FMCAD'13},
  year = 2013,
  pages = {105-112},
  doi = {10.1109/FMCAD.2013.6679398}
}

@inproceedings{Gao:2013:DSS:2523828.2523842,
  author = {Gao, Sicun and Kong, Soonho and Clarke, Edmund M.},
  title = {{dReal}: An {SMT} Solver for Nonlinear Theories over the Reals},
  booktitle = {Automated Deduction},
  series = {CADE'13},
  year = 2013,
  isbn = {978-3-642-38573-5},
  location = {Lake Placid, NY},
  pages = {208--214},
  numpages = 7,
  url = {http://dx.doi.org/10.1007/978-3-642-38574-2_14},
  doi = {10.1007/978-3-642-38574-2_14},
  acmid = 2523842,
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg}
}

@inproceedings{Chaki:2013:CSP:2941729.2941739,
  author = {Chaki, Sagar and Gurfinkel, Arie and Kong, Soonho and Strichman, Ofer},
  title = {Compositional Sequentialization of Periodic Programs},
  booktitle = {Verification, Model Checking, and Abstract Interpretation},
  series = {VMCAI'13},
  year = 2013,
  isbn = {978-3-642-35872-2},
  location = {Rome, Italy},
  pages = {536--554},
  numpages = 19,
  url = {http://dx.doi.org/10.1007/978-3-642-35873-9_31},
  doi = {10.1007/978-3-642-35873-9_31},
  acmid = 2941739,
  publisher = {Springer-Verlag New York, Inc.},
  address = {New York, NY, USA}
}

@inproceedings{Kong:2010:AIQ:1947873.1947904,
  author = {Kong, Soonho and Jung, Yungbum and David, Cristina and Wang, Bow-Yaw and Yi, Kwangkeun},
  title = {Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates},
  booktitle = {Asian Conference on Programming Languages and Systems},
  series = {APLAS'10},
  year = 2010,
  isbn = {978-3-642-17163-5},
  location = {Shanghai, China},
  pages = {328--343},
  numpages = 16,
  url = {http://dl.acm.org/citation.cfm?id=1947873.1947904},
  doi = {10.1007/978-3-642-17164-2_23},
  acmid = 1947904,
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg}
}

@inproceedings{Jung:2010:DIA:2127753.2127771,
  author = {Jung, Yungbum and Kong, Soonho and Wang, Bow-Yaw and Yi, Kwangkeun},
  title = {Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction},
  booktitle = {Verification, Model Checking, and Abstract Interpretation},
  series = {VMCAI'10},
  year = 2010,
  isbn = {978-3-642-11318-5},
  location = {Madrid, Spain},
  pages = {180--196},
  numpages = 17,
  url = {http://dx.doi.org/10.1007/978-3-642-11319-2_15},
  doi = {10.1007/978-3-642-11319-2_15},
  acmid = 2127771,
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg}
}

@inproceedings{Kong:2009:APT:1621607.1621625,
  author = {Kong, Soonho and Choi, Wontae and Yi, Kwangkeun},
  title = {Abstract Parsing for Two-staged Languages with Concatenation},
  booktitle = {Generative Programming and Component Engineering},
  series = {GPCE'09},
  year = {2009},
  isbn = {978-1-60558-494-2},
  location = {Denver, Colorado, USA},
  pages = {109--116},
  numpages = {8},
  url = {http://doi.acm.org/10.1145/1621607.1621625},
  doi = {10.1145/1621607.1621625},
  acmid = {1621625},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {abstract interpretation, multi-staged languages, parsing, program analysis}
}

@inproceedings{KoChYi-PCC-2009,
  author = {Soonho Kong and Wontae Choi and Kwangkeun Yi},
  title = {{PCC} Framework for Program-Generators},
  booktitle = {Workshop on Proof-Carrying Code and Software Certification},
  url = {https://ti.arc.nasa.gov/m/events/pcc09/paper1.pdf},
  year = {2009}
}

@inproceedings{5070712,
  author = {Soonho Kong and Nikolai Tillmann and Jonathan de Halleux},
  booktitle = {Information Technology: New Generations},
  series = {ITNG'09},
  title = {Automated Testing of Environment-Dependent Programs - A Case Study of Modeling the File System for {Pex}},
  year = 2009,
  pages = {758-762},
  keywords = {application program interfaces;file organisation;program testing;software tools;API;Pex;abstraction layer;automated software testing;automated test generation tool;code testing;file system modeling;software developer;software tester;Application software;Automatic testing;File systems;Information technology;Programming profession;Reactive power;Runtime library;Software testing;System testing;Automated Testing;Dynamic Symbolic Execution;Environment Modeling;Test Generation;Unit Testing},
  doi = {10.1109/ITNG.2009.80},
  month = {4}
}