Sungkeun Cho

Compiler Engineer, FuriosaAI
📧 skcho at ropas.snu.ac.kr

Careers

Jan. 2025 - current, Compiler Engineer, FuriosaAI
Jun. 2019 - Jan. 2025, Software Engineer, Meta (formerly Facebook) @ London
Apr. 2017 - Mar. 2019, Contractor (the Static Analysis Tool team), Facebook @ Seoul
Sep. 2009 - Feb. 2018, PhD, ROPAS Laboratory, Department of Computer Science and Engineering, Seoul National University
Advisor: Kwangkeun Yi
Apr. 2002 - Mar. 2006, B.S., Programming Logic Group, College of Information Science, University of Tsukuba

static program analysis, formal verification

ZooBerry: A Software Framework for Global Sparse Analyzers and Their Verified Validators
Inferbo: Infer-Based Buffer Overrun Analyzer
SparrowBerry: A Verified Validator for an Industrial-Strength Static Analyzer
GMeta: A Generic Formal Metatheory Framework for First-Order Representations

Crellvm: Verified Credible Compilation for LLVM. Jeehoon Kang*, Yoonseung Kim*, Youngju Song*, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur**, and Kwangkeun Yi. PLDI'18. [pdf]

* The first three authors contributed equally and are listed alphabetically.
** Hur is the corresponding author.
See more details.
GMeta: A Generic Formal Metatheory Framework for First-Order Representations. Gyesik Lee, Bruno C. d. S. Oliveira, Sungkeun Cho, and Kwangkeun Yi. ESOP'12. [pdf] [bib]

ZooBerry: Automatic Generation of Sparse Global Static Analyzers & Their Validators. Sungkeun Cho and Kwangkeun Yi. PLDI'16 Student Research Competition. [pdf]
Towards Scalable Verified Validation of Static Analyzers. Jeehoon Kang, Sungkeun Cho, Joonwon Choi, and Chung-Kil Hur. APLAS'14. [pdf]
Extensible Verified Validation for LLVM Optimizations. Sungkeun Cho, Joonwon Choi, Jeehoon Kang, Chung-Kil Hur, and Kwangkeun Yi. APLAS'14.

Modified at 2025-01-24 22:01:49