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 : ATVA 2015, 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