Finite Instantiations for Integer Difference Logic. - Hyondeuk Kim; Fabio Somenzi (FMCAD, 2006)

Hybrid CEGAR: combining variable hiding and predicate abstraction. - Chao Wang 001; Hyondeuk Kim; Aarti Gupta (ICCAD, 2007)

Disequality Management in Integer Difference Logic via Finite Instantiations. - Hyondeuk Kim; HoonSang Jin; Fabio Somenzi (J. Satisf. Boolean Model. Comput., 2007)

Application of Formal Word-Level Analysis to Constrained Random Simulation. - Hyondeuk Kim; HoonSang Jin; Kavita Ravi; Petr Spacek; John Pierce; Robert P. Kurshan; Fabio Somenzi (CAV, 2008)

Efficient Term-ITE Conversion for Satisfiability Modulo Theories. - Hyondeuk Kim; Fabio Somenzi; HoonSang Jin (SAT, 2009)