I am studying for a Ph.D. under the supervision of Prof. Edmund Clarke at Computer Science Department, Carnegie Mellon University. My research focuses on the design and implementation of efficient SMT solvers which can handle non-linear real/floating-point arithmetic and their applications to automated theorem proving, embedded/hybrid-system model checking, and static analysis. Here is my [CV].


Contact Info

Awards and Honors

Teaching Experience

Coursework at CMU

Working Experience

Professional Activities

External Reviewer : 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

Extracurricular Activities

May 2009 - Present, English-Korean Translator and Reviewer in TED Open Translation Project