Prof. Kwangkeun Yi Work Address

Rm ***, Bldg ***

Email: abpqhq@r.postjobfree.com School of Computer Science & Engineering

Homepage: ropas.snu.ac.kr/~kwang Seoul National University

*** ******-** ****ak-gu

Seoul 151-744, KOREA

tel: +82 2 880 1857

fax: +82 2 871 4912

Current Position

Professor, School of Computer Science and Engineering

Seoul National University

1993: Ph.D. (Computer Science)

Education Univ. of Illinois at Urbana-Champaign

1987: B.S. (Computer Science & Statistics) Seoul National University

2007 present: Full Professor, Seoul National University

Experience

2003 2007: Associate Professor, Seoul National University

2001 2003: Associate Professor, Korea Advanced Institute of Science & Technology

1995 2001: Assistant Professor, Korea Advanced Institute of Science & Technology

1993 1995: Member of Technical Sta (regular), Software Principles Research Depart-

ment, Bell Labs., Murray Hill, New Jersey, U.S.A.

4/2012 6/2012: Visiting Professor, Laboratory for Computer Science & Arti cial Intel-

ligence, M.I.T., Cambridge, U.S.A. (host: Prof. Arvind and Prof. Martin Rinard)

4/2008 7/2008: Visiting Professor, Laboratory for Computer Science & Arti cial Intel-

ligence, M.I.T., Cambridge, U.S.A. (host: Prof. Martin Rinard)

1/2008 4/2008: Visiting Professor, Computer Science Department, Carnegie-Mellon

University, Pittsburgh, U.S.A. (host: Prof. Edmund Clarke)

7/2002 8/2002: Visiting Professor, Ecole Normale Sup rieure, Paris, France (host: Prof.

e

Patrick Cousot)

7/1998 8/1998: Visiting Research Consultant, Software Principles Research Depart-

ment, Bell Labs., Murray Hill, New Jersey, U.S.A.

9/2008 present: Director, ROSAEC Center (Research On Software Analysis for Error-

free Computing), Engineering Research Center of Excellence, Korea Science & Engineering

Foundation

9/1998 7/2003: Director, ROPAS Center (Research On Program Analysis System),

National Creative Research Initiative Center, Korea Science & Engineering Foundation

Researches semantics-based program analysis

programming language theory

static analysis

higher-order and typed programming language system

programming systems application of static analysis technology

Sparrow: an industrialized static analyzer for static detection of memory errors in C and

Softwares

C++ program sources. It shows superior performance edges against existing competitors

in the market. (http://www.spa-arrow.com)

Airac: a static analyzer for automatic veri cation of bu er overrun errors in C program

sources (http://ropas.snu.ac.kr/airac5).

nML Programming Language System: a dialect of ML (http://ropas.snu.ac.kr/n).

Its compiler system has been used in SNU s and KAIST s programming language classes

since Spring 2000. The Airac analyzer has been implemented in nML.

SML Exception Analyzer: a static analyzer for detecting may-uncaught exceptions in

Standard ML programs. This analyzer has been embedded in the SML/NJ 110 compiler

system and released August 1998.

System Z1, Z2, and Zoo: static program analyzer generator that builds semantic-based

static program analyzers from very high-level speci cations.

Invited seminar, MIT CSAIL, USA, 4/23/2012

Talks

Invited seminar, National Institute of Informatics, Tokyo, Japan, 1/10/2012

Invited seminar, MIT CSAIL, USA, 6/14/2011

Invited seminar, Ecole Normale Sup rieure, Paris, France, 6/09/2011

e

Invited seminar, Oxford Univ., UK, 6/06/2011

Invited seminar, UC Berkeley, USA, 5/31/2011

Invited seminar, Tsinghua University, Beijing, China, 12/02/2010

Invited seminar, Hongkong University of Science and Technology, Hongkong, 11/13/2010

Invited seminar, EADS(European Aeronautic Defence and Space Company), Paris, France,

6/25/2009

Invited talk, International workshop on Program Understanding, Novosibirsk, Russia,

6/15/2009

Invited seminar, SUN Microsystems, Burlington, MA, USA, 6/10/2008

Invited seminar, MIT Lincoln Laboratory, USA, 6/02/2008

Invited seminar, Laboratory for Computer Science and Arti cial Intelligence, MIT, USA,

5/9/2008

Invited seminar, Computer Science Department, Carnegie Mellon University, USA, 2/15/2008

Invited talk, 30 Years of Abstract Interpretation, San Francisco, 1/09/2008,

Invited seminar, School of Computing, National University of Singapore, 10/25/2007

Invited seminar, National Institute of Informatics, Tokyo, Japan, 7/17/2007

Invited seminar, Dagstuhl Seminar 06281 on The Challenge of Software Veri cation,

7/8/2006 - 7/15/2006, Germany

Invited seminar, Dagstuhl Seminar 03101 on Resoning about Shape, 3/2/2003 - 3/7/2003,

Germany

Invited seminar, CRISTAL group, Institut National de Recherche en Informatique et en

Automatique(INRIA), France, 7/4/2002

Visiting Professor, Computer Science Departemnt, Ecole Normale Sup rieure, Paris, 7/1/2002

e

- 8/31/2002

Invited seminar, Computer Science Departemnt, Ecole Normale Sup rieure, Paris, 7/12/2001

e

- 7/14/2001 System Zoo: towards a realistic program analyzer generator

Invited seminar, Dept. of Information Science, Univ. of Tokyo, 3/17/2000 - 3/20/2000

Invited seminar, Static Analysis for Code Compaction and Safety Assurance, Research

Institute of Mathematical Sciences, Kyoto Univ., 3/15/1999 - 3/16/1999

Invited speaker, Static Value Slicing, The 1st Japanese Programming and Programming

Languages Workshop, 3/17/1999 - 3/19/1999

Invited seminar, New Jersey Programming Languages and Systems Seminar Series, Bell

Laboratories, Murray Hill, New Jersey, 7/20/1997 - 7/29/1997

Program Committee Member

POPL 13, ACM Symposium on Principles of Programming Langauges

FOSACS 13, International Conference on Foundations of Softare Science and Computation

Structures

SAS 12, 19th International Static Analysis Symposium

PADL 12, 14th International Symposium on Practical Aspects of Declarative Langauges

PEPM 12, ACM Workshop on Partial Evaluation and Program Manipulation

POPL 12, External Review Committee, ACM Symposium on Principles of Programming

Langauges

CPP 11, First International Conference on Certi ed Programs and Proofs

ESOP 11, The European Symposium on Programming 2010

SSV 10, 5th International Workshop on Systems Software Veri cation

GPCE 10, 9th International Conference on Generative Programming and Component En-

gineering

OOPSLA 10, ACM SIGPLAN International Conference on Object-Oriented Program-

ming, Systems, Languages, and Applications

CAV 10, The 22nd International Conference on Computer Aided Veri cation

VMCAI 10, The 11th International Conference on Veri cation, Model Checking, and Ab-

stract Interpretation 2010

APLAS 09(general chair), The 7th Asian Symposium on Programming Languages and

Systems 2009

SAS 09, The 16th International Static Analysis Symposium

ESOP 09, The European Symposium on Programming 2009

SAS 07, The 14th International Static Analysis Symposium

AWCVS 06, The 1st Asian Working Conference on Veri ed Software

SAS 06(program chair), The 13th International Static Analysis Symposium

CC 06, The 15th International Conference on Compiler Construction

ML 05, The 2005 ACM SIGPLAN Workshop on ML

APLAS 05(program chair), The 3rd Asian Symposium on Programming Languages and

Systems 2005

ESOP 04, The European Symposium on Programming 2004

FLOPS 02, The 6th International Symposium on Functional and Logic Programming 2002

SAS 01, The 8th International Static Analysis Symposium 2001

ICFP 01, ACM SIGPLAN International Conference on Functional Programming 2001

APLAS 03, 04, Asian Symposium on Programming Languages and Systems

ASIAN 98, Asian Computer Science Conference 1998

Publications [International Journals]

LR Error Repair Using the A* Algorithm, Ik-Soon Kim and Kwangkeun Yi, Acta

Informatica, Vol. 47, Issue 3, 2010

Goal-Directed Weakening of Abstract Interpretation Results, Hongseok Yang and Sunae

Seo and Kwangkeun Yi and Taisook Han, ACM Transactions on Programming Lan-

guages and Systems, Vol.29, No.6, Article No.39, October, 2007

Proofs About A Folklore Let-Polymorphic Type Inference Algorithm, Oukseh Lee and

Kwangkeun Yi, ACM Transactions on Programming Languages and Systems,

Vol.20, No.4, pp. 707-723, July 1998

A Cost-e ective Esimation of Uncaught Exceptions in SML Programs, Kwangkeun Yi

and Sukyoung Ryu, Theoretical Computer Science, Vol.277, No.1-2, pp.185-217, 2002

Proof-Directed Debugging Revisited for a First-Order Version Education Pearl, Kwangkeun

Yi, Journal of Functional Programming, Vol.16, No.06, pp.663-670, 2006

Static Insertion of Safe and E ective Memory Reuse Commands into ML-like Programs,

Oukseh Lee and Hongseok Yang and Kwangkeun Yi, Science of Computer Program-

ming, Vol.58, No.1-2, pp.141-178, 2005

An Abstract Interpretation for Estimating Uncaught Exceptions in Standard ML Pro-

grams, Kwangkeun Yi, Science of Computer Programming, Vol.31, No.1, 147-173,

1998

Static Extensivity Analysis for Lambda-De nable Functions over Lattices, Hyunjun Eo

and Kwangkeun Yi and Kwangmoo Choe, New Generation Computing, Vol. 24, No.1,

pp.53-78, 2006

Proofs of a Set of Hybrid Let-Polymorphic Type Inference Algorithms, Hyunjun Eo and

Oukseh Lee and Kwangkeun Yi, New Generation Computing, Vol.22, No.1, pp.1-36,

2004

An Empirical Study on Classi cation Methods for Alarms from a Bug-Finding Static C

Analyzer, Jaewhang Kim and Hosik Choi and Kwangkeun Yi and Yongdae Kim, Infor-

mation Processing Letters, Vol.102, No.2-3, pp.118-123, 2007

A Proof Method for the Correctness of Modularized 0CFA, Oukseh Lee and Kwangkeun

Yi, Information Processing Letters, 81, pp.179-185, 2002

Engaging Students with Theory through ACM Collegiate Programming Contests, Niko-

lay V. Shilov and Kwangkeun Yi, Communications of the ACM, Vol.45, No.9, pp.98-

101, September 2002

Uncaught Exception Analysis for Java, Jangwoo Jo, Byeong-Mo Chang, Kwangkeun Yi,

Kwang-Moo Choe, Journal of Systems and Software, Vol.72, No.1, pp.59-69, 2004

Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles

for Testing Model Checkers, Nikolay Shilov and Kwangkeun Yi, Electronic Notes in

Theoretical Computer Science, Vol 43, 2001

Uni ed Interprocedural Parallelism Detection, Jay Hoe inger and Yunheung Paek and

Kwangkeun Yi, International Journal of Parallel Programming, Vol.29, No.2,

pp.185-215, 2001 (invited paper)

E cient Computation of Fixpoints that Arise in Complex Program Analysis, Li-ling

Chen, Luddy Harrison and Kwangkeun Yi, Journal of Programming Languages,

Vol.3, No.1, pp.31-68, 1995

[International Conferences]

Static Analysis for Multi-Staged Programs via Unstaging Translation, Wontae Choi and

Baris Aktemur and Kwangkeun Yi and Makoto Tatsuda, POPL 2011: The 38th Annual

ACM Sumposium on Principles of Programming languages, Januaray 2011.

A Polymorphic Modal Type System for Lisp-like Multi-Staged Languages, Ik-Soon Kim

and Kwangkeun Yi and Cristiano Calcagno, POPL 2006:The 33rd Annual ACM Sym-

posium on Principles of Programming Languages, pp.257-269, January 2006.

Automatic Generation and Management of Interprocedural Program Analyses, Kwangkeun

Yi and Luddy Harrison, POPL 1993:The Twentieth Annual ACM Symposium on Prin-

ciples of Programming Languages, pp.246-259, January 1993.

Design and Implementation of Sparse Global Analyses for C-like Languages, Hakjoo Oh

and Kihong Heo and Wonchan Lee and Woosuk Lee and Kwangkeun Yi, PLDI 2012:

The 33rd ACM Conference on Programming Language Design and Implementation, June

2012.

The Implicit Calculus: A New Foundation for Generic Programming, Bruno Oliveira

and Tom Schrijvers and Wontae Choi and Wonchan Lee and Kwangkeun Yi, PLDI 2012:

The 33rd ACM Conference on Programming Language Design and Implementation, June

2012.

MeCC: Memory Comparison-Based Clone Detector, Heejung Kim and Yungbum Jung

and Sunghun Kim and Kwangkeun Yi, ICSE 2011: The 33rd International Conference

on Software Engineering, May 2011.

Termination Analysis with Algorithmic Learning, Wonchan Lee and Bow-Yaw Wang

and Kwangkeun Yi, CAV 2012:The International Conference on Computer Aided Veri-

cation, July 2012.

Predicate Generation for Learning-Based Quantifer-free Loop Invariant Inference, Yung-

bum Jung and Wonchan Lee and Bow-Yaw Wang and Kwangkeun Yi, TACAS 2011:

The 17th International Conference on Tools and Algorithms for the Construction and

Analysis of Systems, March 2011.

GMeta: A Generic Formal Metatheory Framework for First-Order Representations

Gyesik Lee and Bruno Oliveira and Sungkeun Cho and Kwangkeun Yi, ESOP 2012:

The 22nd European Symposium on Programming

Automatic Veri cation of Pointer Programs Using Grammar-Based Shape Analysis,

Oukseh Lee and Hongseok Yang and Kwangkeun Yi, Lecture Notes in Computer Sci-

ence, Vol.3444, pp.124-140, ESOP 2005: The European Symposium on Programming,

Edinburgh, April 2-10, 2005

Taming False Alarms from a Domain-Unaware C Analyzer by a Bayesian Statistical Post

Analysis, Yungbum Jung and Jaehwang Kim and Jaeho Shin and Kwangkeun Yi, Lecture

Notes in Computer Science, Vol.3672, pp.203-217, SAS 2005: The 12th International

Static Analysis Symposium, London, September 7-9, 2005

Inserting Safe Memory Reuse Commands into ML-like Programs, Oukseh Lee, Hongseok

Yang, Kwangkeun Yi Lecture Notes in Computer Science, Vol.2694, pp.171-188, SAS

2003: Tenth Annual International Static Analysis Symposium, San Diego, June 11-13,

2003

Towards A Cost-E ective Estimation of Uncaught Exceptions in SML Programs, Kwangkeun

Yi and Sukyoung Ryu, Lecture Notes in Computer Science, Vol. 1302, pp.98-113, SAS

1997: The 4th International Static Analysis Symposium, Paris, Sept. 1997

Compile-time Detection of Uncaught Exceptions in Standard ML Programs, Kwangkeun

Yi, Lecture Notes in Computer Science, Vol. 864, pp.238-254, SAS 1994: The 1st In-

ternational Static Analysis Symposium, Namur, Sept. 1994

Sound Non-Statistical Clustering of Static Analysis Alarms, Woosuk Lee and Wonchan

Lee and Kwangkeun Yi, VMCAI 2012: The 13th International Conference on Veri ca-

tion, Model Checking, and Abstract Interpretation

Access Analysis-Based Tight Localization of Abstract Memories, Hakjoo Oh and Lu-

cas Brutschy and Kwangkeun Yi, VMCAI 2011:The 12th International Conference on

Veri cation, Model Checking, and Abstract Interpretation, January 2011.

Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Ab-

straction, Yungbum Jung and Soonho Kong and Bow-Yaw Wang and Kwangkeun Yi,

VMCAI 2010:The 11th International Conference on Veri cation, Model Checking, and

Abstract Interpretation, January 2010.

Static Monotonicity Analysis for Lambda-de nable Functions over Lattices, Andrzej

Murawski and Kwangkeun Yi, Lecture Notes in Computer Science, Vol.2294, pp.139-153,

VMCAI 2002: Third International Workshop on Veri cation, Model Checking and Ab-

stract Interpretation, Venice, January 21-22, 2002

A Practical Memory Leak Detector Based on Parameterized Procedural Summaries,

Youngbum Jung and Kwangkeun Yi, ISMM 2008: ACM SIGPLAN 2008 International

Symposium on Memory Management, June 2008.

Experiments on the E ectiveness of an Automatic Insertion of Safe Memory Reuses

into ML-like Programs, Oukseh Lee and Kwangkeun Yi, ISMM 2004: The 2004 ACM

International Symposium on Memory Management, Vancouver, October 24-25, 2004 (also

at SPACE 2004, the Second ACM/SIGPLAN Workshop on Semantics, Program Analysis,

and Computing Environments for Memory Management, Venice, January 12, 2004)

Access-Based Localization with Bypassing, Hakjoo Oh and Kwangkeun Yi, APLAS

2011: The 9th Asian Symposium on Programming Langauges and Systems

Type and E ect System for Multi-Staged Exceptions Hyunjun Eo and Ik-Soon Kim and

Kwangkeun Yi, Lecture Notes in Computer Science, Vol.4279, pp.61-78, APLAS 2006:

The 4th Asian Symposium on Programming Languages and Systems, November 8-10, 2006

Automatic Construction of Hoare Proofs from Abstract Interpretation Results, Sunae

Seo and Hongseok Yang and Kwangkeun Yi, Lecture Notes in Computer Science, Vol.2895,

pp.230-245, APLAS 2003: The First Asian Symposium on Programming Languages and

Systems, Beijing, November 27-29, 2003

Proving Syntactic Properties of Exceptions in an Ordered Logical Framework, Je

Polakow and Kwangkeun Yi, Lecture Notes in Computer Science, Vol.2024, pp. 61-77,

FLOPS 2001: Proceedings of the 5th International Symposium on Functional and Logic

Programming, March, 2001

Soundness by Static Analysis and False-alarm Removal by Statistical Analysis: Our

Airac Experience, Yungbum Jung and Jaehwang Kim and Jaeho Shin and Kwangkeun Yi,

Bugs 2005: Workshop on the Evaluation of Software Defect Detection Tools, Chicago,

June 12, 2005

Assessing the Overhead of ML Exceptions by Selective CPS Transformation, Jung-taek

Kim, Kwangkeun Yi, Olivier Danvy, ML 1998: The 1998 ACM SIGPLAN Workshop on

ML, pp.103-114, Baltimore, Sept., 1998

Exception Analysis for Multithreaded Java Programs, Sukyoung Ryu and Kwangkeun

Yi, APAQS 2001: The Second Asia-Paci c Conference on Quality Software, Hongkong,

pp.23-32, December 2001

Interconnecting Between CPS Terms and Non-CPS Terms, CW 2001: The Proceedings

of the Third ACM SIGPLAN Workshop on Continuations, Jung-taek Kim and Kwangkeun

Yi, January, 2001

Interprocedural Exception Analysis for Java, Byeong-Mo Chang and Jangwoo Jo and

Kwangkeun Yi and Kwang-Moo Choe, The Proceedings of the 16th ACM Symposium on

Applied Computing, March, 2001

Constraint-based Analysis for Java, Byeong-Mo Chang and Kwangkeun Yi and Jang-

woo Jo, SSGRR Conference on Computers and E-Business, L Aquila, Italy, August, 2000

(invited presentation)

Escape Analysis for Stack Allocation in Java, Eunsun Cho and Kwangkeun Yi, ECOOP 00

Workshop on Formal Techniques for Java Programs, June, 2000

Exception Analysis for Java, Kwangkeun Yi and Byeong-Mo Chang, Lecture Notes in

Computer Science, Vol.1743, pp.111-112 ECOOP 99 Workshop on Formal Techniques for

Java Programs, June, 1999

SUIF Program Analysis Using System Z2, Seong-Hoon Kim, Kwangkeun Yi, Hyun-jun

Eo, Kwang-Moo Choe, Proceedings of The Second SUIF Compiler Workshop, Aug., 1997

Estimating Uncaught Exceptions in Standard ML Programs from Type-based Equa-

tions, Kwangkeun Yi and Sukyoung Ryu and Ki-Hyun Pyun, Proceedings of the 20th An-

nual International Computer Software and Applications Conference, pp. 455-460, Seoul,

August 1996

Automatic Generation and Management of Program Analyses, Kwangkeun Yi, Ph.D. The-

sis, Report UIUCDCS-R-93-1828, Univ. of Illinois at Urbana-Champaign, August 1993.

On-the- y Circuits to Measure the Average Working Set Size Kwangkeun Yi and Luddy

Harrison, Proceedings of the IEEE International Conference on Computer Design: VLSI

in Computers and Processors, Cambridge, September 1990.

[Book Chapters]

How to nd a coin: propositional program logics made easy, Nikolay Shilov and Kwangkeun

Yi, Current Trends in Theoretical Computer Science, Vol.2: Formal Models and Seman-

tics, pp.181-214, April 2004, World Scienti c, Edited by G. Paun, G. Rozenberg, and A.

Salomaa

Teaching Classes

SNU 4541.664A: Program Analysis (graduate)

SNU 4541.780: Topics in Programming Language (graduate)

SNU 4190.310: Programming Languages (undergraduate)

SNU 4190.210: Principles of Programming (undergraduate)

SNU 400.02: Engineering Math II: Logic in Computing (undergraduate)

SNU 010.142: Basics in Computing (undergraduate)

Hosting Visiting Ph.D. Students & Post-docs

Ludovic Patey, 3/2011 - 8/2011, 10/2011-2/2012, Ph.D. student, Ecole Normale Sup rieure,

e

Paris, France

Cristian Gherghina, 6/2011 - 9/2011, Ph.D. student, National Univ. of Singapore

Saransh Srivastava, 5/2011 - 7/2011, undergraduate, Indian Institute of Technology, Kan-

pur, India

Ning Chen, 6/2010 - 8/2010, Ph.D. student, Computer Science, Hongkong University of

Science and Technology, China

Bow-Yaw Wang, 6/2010 - 8/2010, Ph.D., Institute of Information Science, Academia

Sinica, Taiwan

Ben Lickly, 5/2010 - 8/2010, Ph.D. student, EECS, UC Berkeley

Cristina David, 10/2009 - 12/2009, Ph.D. student, Computer Science, National Univ. of

Singapore

Lucas Brutschy, 9/2009 - 3/2010, M.S. student, Computer Science, Aachen University,

Germany

Will Klieber, 5/2009 - 8/2009, Ph.D. student, Computer Science, Carnegie-Mellon Uni-

versity

Pascal Cuoq, 12/2002 - 12/2003, Ph.D., INRIA, France

Andrzej Murawski, 7/6/2001 - 8/5/2001, Ph.D. student, Oxford Univ.

Je Sarnat, 6/4/2001 - 8/19/2001, senior undergraduate, Carnegie-Mellon University

Je Polakow, 6/20/2000 - 8/20/2000, Ph.D. student, Carnegie-Mellon University

Fermin Reig, 7/21/2000 - 10/20/2000, Ph.D. student, Univ. of Glasgow

Charles Hymans, 8/1/1999 - 1/30/2000, Ph.D. student, Ecole Normale Sup rieure

e

6/2007: 17th Annual Distinguished Scienti c and Technological Paper Award, The Korea

Honors

Federation of Science and Technology Societies

9/1998 7/2003: Directorship, Center for Research On Program Analysis System, Na-

tional Creative Research Initiative Grant Program, Korea Ministry of Science and Tech-

nology

9/2001: Kaheon Academic Excellence Award, Korea Information Science Society

1984 1986: Undergraduate Fellow, Korea Foundation for Advanced Studies

1983: 1st-ranked in entrance exam, Division of Mathematics, Computer Science, and

Statistics, College of Natural Science, Seoul National University

Contact this candidate