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 at New York University currently working with Thomas Wies and previously with Benjamin Goldberg, and one of the members of Analysis of Computer Systems Group (ACSys).

I have been 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 incremental SAT solving, having commercialized parallelized high-performance dynamic constraint solving system. Likewise, I am in general interested in any subjects related to SAT including parallel 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/localization using error invariants, which are computed by Craig interpolantion.


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

Oh, Chanseok, Martin Schaf, Daniel Schwartz-Narbonne, and Thomas Wies. "Concolic Fault Abstraction." To appear in Proc. of the 14th IEEE International Working Conference on Source Code Analysis and Manipulation.
Ezick, James, Jonathan Springer, Tom Henretty, and Chanseok Oh. "Extreme SAT-based Constraint Solving with R-Solve." To appear in Proc. of the 18th IEEE High Performance Extreme Computing Conference.
Oh, Chanseok. "MiniSat_HACK_999ED, MiniSat_HACK_1430ED and SWDiA5BY." In Proc. of the SAT Competition 2014: Solver and Benchmark Descriptions. Dept. of Computer Science Series of Publications B, University of Helsinki, vol. B-2014-2, 2014, pp. 46.
Oh, Chanseok. "gluH: modified version of gluclose 2.1." In Proc. of the SAT Competition 2013: Solver and Benchmark Descriptions. Dept. of Computer Science Series of Publications B, University of Helsinki, vol. B-2013-1, 2013, pp. 48.
Oh, Chanseok. "Variable elimination algorithm for model counting for #SAT." In Proc. of the 3rd International Conference on Advanced Topics in Artificial Intelligence. GSTF, 2012, pp. 6-12. Best Student Paper Award.

WORKSHOPS

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

HONORS & REWARDS

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


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 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