이 광근 Kwangkeun Yi's Papers

Papers [Copyright Notice]

(topics in alphabetical order)


automatic bug detection for C programs	program transformation
exception analysis	staged programming languages
heap analysis	static analysis and certification
other static analyses	static analysis tools
program logics	type systems

(For journal/conference categorization: click here)

Automatic bug detection for C programs

실제 C 프로그램의 소스 오류를 자동으로 미리 찾아내는 분석기에 대해서.
Works on sound and automatic detection of bugs in realistic C programs.

A Practical Memory Leak Detector Based on Parameterized Procedural Summaries
[pdf/ bibtex]
Youngbum Jung and Kwangkeun Yi
ISMM 2008: ACM SIGPLAN 2008 International Symposium on Memory Management, Tucson, June 7-8, 2008
An Empirical Study on Classification Methods for Alarms from a Bug-Finding Static C Analyzer
[pdf/ bibtex ]
Kwangkeun Yi and Hosik Choi and Jaehwang Kim and Yongdai Kim
Information Processing Letters, Vol.102, No.2-3, pp.118-123, 2007
"Proof-Directed Debugging" Revisited for a First-Order Version
[pdf/ bibtex ]
Kwangkeun Yi
Journal of Functional Programming, Vol. 16, No. 06, pp. 663-670, 2006
Taming False Alarms from a Domain-Unaware C Analyzer by a Bayesian Statistical Post Analysis
[pdf/ bibtex]
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
Soundness by Static Analysis and False-alarm Removal by Statistical Analysis: Our Airac Experience
[pdf/ bibtex]
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

Exception analysis

프로그램에서 처리되지않는 예외상황들을 예측해내는 방법에 대해서.
Works on estimating uncaught exceptions in programs

Type and Effect System for Multi-Staged Exceptions
[pdf/ bibtex ]
Hyunjun Eo and Ik-Soon Kim and Kwangkeun Yi
APLAS 2006: 4th Asian Symposium on Programming Languages and Systems, November 8-10, 2006.
Lecture Notes in Computer Science, Vol.4279, pp. 61-78.
An Uncaught Exception Analysis for Java
[pdf/ bibtex]
Jangwoo Jo, Byeong-Mo Chang, Kwangkeun Yi, Kwang-Moo Choe
Journal of Systems and Software, Vol.72, No.1, pp.59-69, 2004
A Cost-effective Estimation of Uncaught Exceptions in SML Programs
[pdf / bibtex]
Kwangkeun Yi and Sukyoung Ryu
Theoretical Computer Science, Vol. 277, No.1-2, pp.185-217, 2002 (invited paper)
Exception Analysis for Multithreaded Java Programs
[pdf/ bibtex]
Sukyoung Ryu and Kwangkeun Yi
APAQS 2001: The Second Asia-Pacific Conference on Quality Software , December, 2001
Interprocedural Exception Analysis for Java
[ps.gz/ bibtex]
Byeong-Mo Chang and Jangwoo Jo and Kwangkeun Yi and Kwang-Moo Choe
16th ACM Symposium on Applied Computing, March, 2001
Exception Analysis for Java
[ps.gz / dvi.gz / bibtex]
Kwangkeun Yi and Byeong-Mo Chang
ECOOP'99 Workshop on Formal Techniques for Java Programs, June, 1999
Lecture Notes in Computer Science, Vol.1743, pp.111-112
Object-Oriented Technology. ECOOP'99 Workshop Reader.
Towards A Cost-Effective Estimation of Uncaught Exceptions in SML Programs
[ps.gz / dvi.gz / bibtex]
Kwangkeun Yi and Sukyoung Ryu
Lecture Notes in Computer Science, Vol. 1302, pp.98-113
The 4th International Static Analysis Symposium , Paris, Sept. 1997, (talk slides)
Estimating Uncaught Exceptions in Standard ML Programs from Type-based Equations
[ps.gz / dvi.gz / bibtex]
Kwangkeun Yi and Sukyoung Ryu and Ki-Hyun Pyun
The 20th Annual International Computer Software and Applications Conference, pp. 455-460, Seoul, August 1996
An Abstract Interpretation for Estimating Uncaught Exceptions in Standard ML Programs
[ps.gz / dvi.gz / bibtex]
Kwangkeun Yi
Science of Computer Programming, Vol.31, No.1, pp.147-173, 1998 (invited paper)
Compile-time Detection of Uncaught Exceptions in Standard ML Programs
[ps.gz / dvi.gz / bibtex]
Kwangkeun Yi
Lecture Notes in Computer Science, Vol. 864, pp.238-254
The 1st International Static Analysis Symposium, Namur, Sept. 1994

Heap analysis

프로그램이 만드는 메모리 구조물의 성질을 예측하는 방법에 대해서.
Works on static estimation of the properties of program's dynamic memory structures.

Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis
[pdf/ bibtex]
Oukseh Lee and Hongseok Yang and Kwangkeun yi
Lecture Notes in Computer Science, Vol.3444, pp.124-140
ESOP 2005: The European Symposium on Programming, Edinburgh, April 2-10, 2005
Experiments on the Effectiveness of an Automatic Insertion of Safe Memory Reuses into ML-like Programs
[pdf/ bibtex]
Oukseh Lee and Kwangkeun Yi
ISMM 2004: ACM International Symposium on Memory Management, pp.97-107, Vancouver, October 24-25, 2004
An old version was also presented at: SPACE 2004, the Second ACM/SIGPLAN Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management, Venice, January 12, 2004 [pdf/ bibtex]
Static Insertion of Safe and Effective Memory Reuse Commands into ML-like Programs
[pdf/ bibtex]
Oukseh Lee and Hongseok Yang and Kwangkeun Yi
Science of Computer Programming, Vol. 58, No.1-2, pp.141-178, October 2005
Inserting Safe Memory Reuse Commands into ML-like Programs
[pdf/ bibtex]
Oukseh Lee and Hongseok Yang and Kwangkeun Yi
Lecture Notes in Computer Science, Vol.2694, pp.171-188
Tenth Annual International Static Analysis Symposium, San Diego, June 11-13, 2003

Static Analysis and Certification

프로그램 분석을 프로그램 검증에 적용하는 방향에 대해서.
Works on using static analysis for program certification or verification.

Goal-Directed Weakening of Abstract Interpretation Results
[pdf/ bibtex ]
Sunae Seo and Hongseok Yang and Kwangkeun Yi and Taisook Han
ACM Transactions on Programming Languages and Systems, Vol.29, No.6, Article No.39, Oct. 2007
Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis
[pdf/ bibtex]
Oukseh Lee and Hongseok Yang and Kwangkeun yi
Lecture Notes in Computer Science, Vol.3444, pp.124-140
ESOP 2005: The European Symposium on Programming, Edinburgh, April 2-10, 2005
Automatic Construction of Hoare Proofs from Abstract Interpretation Results
[pdf/ bibtex]
Sunae Seo and Hongseok Yang and Kwangkeun Yi
Lecture Notes in Computer Science, Vol.2895, pp.230-245
The First Asian Symposium on Programming Languages and Systems, Beijing, November 27-29, 2003

Static Analysis Tools

프로그램 성질을 분석하는 프로그램을 만들어주는 시스템에 대해서.
Works on automatic generations and management of program analyses

Static Monotonicity Analysis for Lambda-definable Functions over Lattices
[pdf/ bibtex]
Andrzej Murawski and Kwangkeun Yi
Lecture Notes in Computer Science, Vol.2294, pp.139-153
Third International Workshop on Verification, Model Checking and Abstract Interpretation, Venice, January 21-22, 2002
Yet Another Ensemble of Abstract Interpreter, Higher-Order Data-Flow Equations, and Model Checking
[ps.gz / bibtex]
Kwangkeun Yi
ROPAS Technical Memorandum No.2001-10, March, 2001
SUIF Program Analysis Using System Z2
[ps.gz / dvi.gz / bibtex]
Seong-Hoon Kim, Kwangkeun Yi, Hyun-jun Eo, and Kwang-Moo Choe
The Second SUIF Compiler Workshop, Aug. 21 - 23, 1997
Efficient Computation of Fixpoints that Arise in Complex Program Analysis
[ps.gz / dvi.gz / bibtex]
Li-ling Chen, Luddy Harrison and Kwangkeun Yi
Journal of Programming Languages, Vol.3, No.1, pp.31-68, 1995
Automatic Generation and Management of Interprocedural Program Analyses
[ps.gz / dvi.gz / bibtex]
Kwangkeun Yi and Luddy Harrison
The 20th ACM Symposium on Principles of Programming Languages, pp. 246-259, Jan. 1993
Automatic Generation and Management of Program Analyses
[ps.gz / bibtex]
Kwangkeun Yi
Ph.D. Thesis, Report UIUCDCS-R-93-1828
System Z1 Programming Manual
Kwangkeun Yi and Luddy Harrison
CSRD Report No 1283
Interprocedural Data Flow Analysis for Compile-Time Memory Management Kwangkeun Yi and Luddy Harrison
CSRD Report No 1244

Program Logics

프로그램 논리와 모델검증에 대해서.
Works on program logics and model checking.

How to find a coin: propositional program logics made easy
[ps/ bibtex]
Nikolay Shilov and Kwangkeun Yi
Current Trends in Theoretical Computer Science, Vol.2: Formal Models and Semantics, pp. 181-214, April 2004, World Scientific
Edited by G. Paun, G. Rozenberg, and A. Salomaa
Program Logics Made Easy
Nikolay Shilov and Kwangkeun Yi
ROPAS Technical Memorandum, No. 2000-7, KAIST, March, 2001
A Note on Model Checking Reuse
[ps.gz/ bibtex]
Nikolay Shilov and Kwangkeun Yi
2nd Australian Workshop on Computational Logic AWCL'01, Gold Cost, Australia, Jan 31 - Feb 1, 2001
Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles for Testing Model Checkers
[pdf/ ps/ bibtex]
Nikolay Shilov and Kwangkeun Yi
Electronic Notes in Theoretical Computer Science, Vol 43, 2001
On Expressive and Model Checking Power of Propositional Program Logics
[ps/ bibtex]
Nikolay Shilov and Kwangkeun Yi
Lecture Notes in Computer Science, Vol.2244, pp.39-46
Perspectives of System Informatics: 4th International Andrei Ershov Memorial Conference, 2001
How To Find A Coin: Propositional Program Logics Made Easy.
[ps/ bibtex]
Nikolay Shilov and Kwangkeun Yi
Bulletin of the European Association for Theoretical Computer Science, Vol.75, pp.127-151, 2001
A New Proof of Exponential Decidability for Propositional Mu-Calculus with Program Converse
[ps.gz/ bibtex]
Nikolay Shilov and Kwangkeun Yi
III International Conference on Theoretical Aspects of Computer Science, Novi Sad, Yugoslavia, Sep 4-7, 2000
Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles for Testing Model Checkers
[ps.gz/ bibtex]
Nikolay Shilov and Kwangkeun Yi
Formal Methods *ELSEWHERE* , a Satellite Workshop of FORTE-PSTV-2000, Pisa, Italy, Oct 10, 2000
Model Checking Puzzles in Mu-Calculus
[ps.gz/ bibtex]
Nikolay Shilov and Kwangkeun Yi
Joint Bulletin of the Novosibirsk Computing Center and A.P.Ershov Institute of Informatics Systems, No. 13, 2000

Program Transformation

프로그램 변환에 대해서.
Works on program transformations.

Interconnecting Between CPS Terms and Non-CPS Terms
[ps.gz/ dvi.gz/ bibtex]
Jung-taek Kim and Kwangkeun Yi
The Third ACM SIGPLAN Workshop on Continuations (CW'01), London, Jan. 16, 2001
CPS Transformation after Exception Analysis
Jung-taek Kim and Kwangkeun Yi and Olivier Danvy and Lasse R. Nielsen
Assessing the Overhead of ML Exceptions by Selective CPS Transformation
[ps.gz / dvi.gz / bibtex]
Jung-taek Kim and Kwangkeun Yi and Olivier Danvy
The 1998 ACM SIGPLAN Workshop on ML, pp.103-114, Baltimore, Sept., 1998
(also as a technical report of the BRICS)

Staged Programming Languages

A Polymorphic Modal Type System for Lisp-like Multi-Staged Languages
Ik-Soon Kim and Kwangkeun Yi and Cristiano Calcagno
[pdf/ bibtex]
POPL 2006: The 33rd Annual ACM Symposium on Principles of Programming Languages , pp. 257-268, January 11-13, 2006.
Type and Effect System for Multi-Staged Exceptions
[pdf/ bibtex ]
Hyunjun Eo and Ik-Soon Kim and Kwangkeun Yi
APLAS 2006: 4th Asian Symposium on Programming Languages and Systems, November 8-10, 2006.
Lecture Notes in Computer Science, Vol.4279, pp. 61-78.

Type inference

프로그래밍 언어의 타입 유추 알고리즘에 대해서.
Works on type inference algorithms

Proofs of a Set of Hybrid Let-Polymorphic Type Inference Algorithms
[ps.gz/ bibtex]
Hyunjun Eo and Oukseh Lee and Kwangkeun Yi
New Generation Computing, Vol.22, No.1, pp.1-36, 2004
Proofs About A Folklore Let-Polymorphic Type Inference Algorithm
[ps.gz / dvi.gz / bibtex]
Oukseh Lee and Kwangkeun Yi
ACM Transactions on Programming Languages and Systems, Vol. 20, No. 4, pp. 707-723, July 1998
A Generalized Let-Polymorphic Type Inference Algorithm
[ps / ps.gz / dvi.gz / pdf / bibtex ]
Oukseh Lee and Kwangkeun Yi
Technical Memo. ROPAS-2000-5, Research On Program Analysis System, KAIST, March 2000

Other Static Analyses

LR Error Repair Using the A* Algorithm
[pdf/ bibtex]
Ik-Soon Kim and Kwangkeun Yi
Acta Informatica, 2010
Static Extensivity Analysis for Lambda-definable Functions over Lattices
[ps/bibtex]
Hyunjun Eo and Kwangkeun Yi and Kwangmoo Choe
New Generation Computing Vol.24, No.1, pp.53-78, 2006
Static Monotonicity Analysis for Lambda-definable Functions over Lattices
[pdf/ bibtex]
Andrzej Murawski and Kwangkeun Yi
Lecture Notes in Computer Science, Vol.2294, pp.139-153
Third International Workshop on Verification, Model Checking and Abstract Interpretation, Venice, January 21-22, 2002
A Proof Method for the Correctness of Modularized 0CFA
[pdf / bibtex]
Oukseh Lee, Kwangkeun Yi, Yunheung Paek
Information Processing Letters 81 (2002), pp. 179-185
Engaging Students with Theory through ACM Collegiate Programming Contests
[pdf / bibtex]
Nikolay Shilov and Kwangkeun Yi
Communications of the ACM, Vol.45, No.9, pp.98-101, September, 2002
Proving Syntactic Properties of Exceptions in an Ordered Logical Framework
[ps.gz / bibtex]
Jeff Polakow and Kwangkeun Yi
Lecture Notes in Computer Science, Vol.2024, pp.61-77
The Fifth International Symposium on Functional and Logic Programming (FLOPS'01), Tokyo, March, 2001
Constraint-based Analysis for Java
[ps.gz / bibtex]
Byeong-Mo Chang and Kwangkeun Yi and Jangwoo Jo
SSGRR Conference on Computers and E-Business, L'Aquila, Italy, August, 2000
Escape Analysis for Stack Allocation in Java
[ps.gz / bibtex]
Eunsun Cho and Kwangkeun Yi
ECOOP'00 Workshop on Formal Techniques for Java Programs, Canne, France, June, 2000
Unified Interprocedural Parallelism Detection
[ps.gz]
Jay Hoeflinger, Yunheung Paek, Kwangkeun Yi
International Journal of Parallel Programming, Vol.29, No.2, pp. 185-215, April, 2001
On-the-fly Circuits to Measure the Average Working Set Size
Kwangkeun Yi and Luddy Harrison
IEEE International Conference on Computer Design: VLSI in Computers and Processors, Sept. 1990 (Look for it here)