Hyondeuk Kim

• Address:
  University of Colorado
  Dept. of Electrical and Computer Engineering
  Campus Box 425
  Boulder CO, 80309-0425
  U.S.A.
• E-mail: Hyondeuk.Kim _at_ Colorado _dot_ EDU

About

• I am a Ph.D. student in the Department of Electrical, Computer, and Energy Engineering (ECEE) at the University of Colorado at Boulder. I am working with Prof. Fabio Somenzi in VLSI/CAD RESEARCH GROUP.

Research interests

• SMT solvers, SAT solvers, Theorem Proving, Formal Verification.

Publications

• "Efficient Term ITE Conversion for Satisfiability Modulo Theories", H. Kim, F. Somenzi, H. Jin. Twelfth International Conference on Theory and Applications of Satisfiability Testing (SAT'09) [pdf]


• "Application of Formal Word-Level Analysis to Constrained Random Simulation", H. Kim, H. Jin, K. Ravi, P. Spacek, J. Pierce, B. Kurshan, F. Somenzi. 20th International Conference on Computer Aided Verification (CAV'08) [pdf]


• "Hybrid CEGAR: combining variable hiding and predicate abstraction", C. Wang, H. Kim, A. Gupta. International Conference on Computer Aided Design (ICCAD'07) [pdf]


• "Disequality Management in Integer Difference Logic via Finite Instantiations", H. Kim, H. Jin, F. Somenzi. Journal on Satisfiability, Boolean Modeling and Computation (JSAT'07) [pdf]


• "Finite Instantiations for Integer Difference Logic", H. Kim, F. Somenzi. International Conference on Formal Methods in Computer Aided Design (FMCAD'06) [pdf]

SatEEn: SAT Enumeration ENgine

• SatEEn is an SMT (Satisfiability Modulo Theories) solver that deals with Quantifier-Free Linear Arithmetic Logic and Quantifier-Free Difference Logic.

CirCUs: Hybrid Satifiability solver

• CirCUs is a SAT solver based on the DPLL procedure and conflict clause recording.

VIS: A system for Verification and Synthesis

• VIS is a symbolic model checker.

Personal

• Tennis.