Chanseok Oh

Ph.D. Candidate

Computer Science Department
Courant Institute of Mathematical Sciences
Graduate School of Arts and Science
New York University


Warren Weaver Hall, Room 410
251 Mercer Street
New York, NY 10012


Office+1-212-998-3079
Mobile+1-917-885-8777
Email My first name, chanseok, followed by the department domain, @cs.nyu.edu

Welcome! I am a Ph.D. student in Analysis of Computer Systems Group (ACSys) at New York University currently working with Thomas Wies and previously with Benjamin Goldberg.

I have dedicated most of my PhD years to the study of the fundamental problem of satisfiability of boolean logic (SAT), with the particular focus on practical SAT solving and improving state-of-the-art SAT solvers. Relevantly, I have also been working closely with Reservoir Labs on the subject of "unrestricted" incremental SAT, having commercialized a parallelized high-performance dynamic constraint solving system. Likewise, I am in general interested in any subjects related to SAT, and in a broader sense, computationally hard constraint satisfaction and optimization problems from both practical and theoretical perspectives. I am also greatly interested in Satisfiability Modulo Theories (SMT) (where an SMT solver uses a SAT solver at its core) and accordingly, related subjects such as decision procedures, automated reasoning, and logic in general.

As a member of ACSys, my research interests also cover usual topics in formal methods, and my current research includes fault analysis/bug localization using error invariants, which are computed by Craig interpolation.


BACKGROUND

2009 - PresentNew York University, New York, NY
Ph.D. Candidate in Computer Science
1999 - 2006 Korea Advanced Institute of Science and Technology, Korea
B.S. in Computer Science
magna cum laude

PUBLICATIONS

Daniel Schwartz-Narbonne, Chanseok Oh, Martin Schäf, and Thomas Wies. "VERMEER: A Tool for Tracing and Explaining Faulty C Programs." To appear in Proc. of the 37th International Conference on Software Engineering (ICSE'15).
Chanseok Oh, Martin Schäf, Daniel Schwartz-Narbonne, and Thomas Wies. "Concolic Fault Abstraction." In Proc. of the 14th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM'14).
James Ezick, Jonathan Springer, Tom Henretty, and Chanseok Oh. "Extreme SAT-based Constraint Solving with R-Solve." In Proc. of the 18th IEEE High Performance Extreme Computing Conference (HPEC'14).
Chanseok Oh. "MiniSat_HACK_999ED, MiniSat_HACK_1430ED and SWDiA5BY." In Proc. of the SAT Competition 2014: Solver and Benchmark Descriptions (SAT-COMP'14).
Chanseok Oh. "gluH: modified version of gluclose 2.1." In Proc. of the SAT Competition 2013: Solver and Benchmark Descriptions (SAT-COMP'13).
Chanseok Oh. "Variable elimination algorithm for model counting for #SAT." In Proc. of the 3rd International Conference on Advanced Topics in Artificial Intelligence (ATAI'12). Best Student Paper Award.

WORKSHOPS

Chanseok Oh, Martin Schäf, Daniel Schwartz-Narbonne, and Thomas Wies. "Fault Localization using Interpolation." At the 2nd Workshop on Interpolation: From Proofs to Applications (iPRA'14). [slides]

HONORS & AWARDS

FLoC Olympic Games | Vienna Summer of Logic
SAT Competition 2014 (SAT-COMP'14)
Gold, Minisat Hack Track
Silver, Application SAT+UNSAT Track
Bronze, Application SAT Track
Bronze, Application UNSAT Track
Configurable SAT Solver Challenge 2014 (CSSC'14)
Silver, Industrial SAT+UNSAT Track
Bronze, Random SAT+UNSAT Track
Best Student Paper Award. At the 3rd International Conference on Advanced Topics in Artificial Intelligence (ATAI'12).

TOOLS

  • MiniSat_HACK_999ED, MiniSat_HACK_1430ED, and SWDiA5BY: downloadable from the EDACC system through the SAT Competition 2014 website.
  • R-Solve: Parallelized High-performance Dynamic Constraint Solving System

TEACHING

Graduate Courses at New York University
Summer 2013,Adjunct Instructor, CSCI-GA.2110 Programming Languages Recitation
Spring 2013,Adjunct Instructor, CSCI-GA.2110 Programming Languages Recitation
Fall 2012,Adjunct Instructor, CSCI-GA.2110 Programming Languages Recitation
Summer 2012,Adjunct Instructor, CSCI-GA.2110 Programming Languages Recitation
Summer 2011,Adjunct Instructor, CSCI-GA.2110 Programming Languages Recitation
Undergraduate Courses at New York University
Spring 2011,Adjunct Instructor, CSCI-UA.0102 Data Structures Recitation

PROFESSIONAL EXPERIENCE

May 2015 - Aug 2015     Google, Intern
May 2014 - Aug 2014     Google, Intern
Sep 2013 - Jan 2014     Reservoir Labs, Research Intern
Jan 2006 - May 2008     Oracle, Technical Support Engineer
Aug 2003 - Feb 2005     Daum Communications, Software Engineer
Jul 2002 - Aug 2003     EK-Project, Ltd, Software Developer
Apr 2000 - Jul 2000     Caldera Linux, Part-time Software Localization Engineer

CERTIFICATES

Oracle Certified Professional, Oracle Corporation
Oracle Certified Associate, Oracle Corporation
Certificate of Information Processing Engineer, HR Developement Service of Korea

SCHOLARSHIP

2009 - 2014     McCracken Fellowship, New York University