Papers by Topics

Most recent papers that are always available from here may not yet be reflected in this page.

Papers are categorized by topics or journal/conference.

• Automatic Bug Detection for C Program (8)
• Exception Analysis (10)
• Heap Analysis (4)
• Program Analysis Tools (10)
• Program Logics (11)
• Program Transformation (3)
• Separation Logic (5)
• Staged Programming Languages (3)
• Syntactic Analysis (1)
• Type Systems (2)
• Other Program Analyses (11)

Automatic Bug Detection for C Program

Works on sound and automatic detection of bugs in realistic C programs.

• "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: 33rd ACM Conference on Programming Language Design and Implementation. 2012.
  [ pdf / BibTeX ]
• "Access Analysis-Based Tight Localization of Abstract Memories."
  Hakjoo Oh and Lucas Brutschy and Kwangkeun Yi.
  VMCAI 2011: 12th International Conference on Verification, Model Checking, and Abstract Interpretation. 2011. pp. 356--370.
  [ pdf / BibTeX ]
• "Access-Based Localization with Bypassing."
  Hakjoo Oh and Kwangkeun Yi.
  APLAS 2011: 9th Asian Symposium on Programming Languages and Systems. 2011. pp. 50--65.
  [ pdf / BibTeX ]
• "Practical memory leak detector based on parameterized procedural summaries."
  Yungbum Jung and Kwangkeun Yi.
  ISMM. 2008. pp. 131-140.
  [ pdf / BibTeX ]
• "An Empirical Study on Classification Methods for Alarms from a Bug-Finding Static C Analyzer."
  Kwangkeun Yi and Hosik Choi and Jaehwang Kim and Yongdai Kim.
  Information Processing Letters. 102 (2-3). 2007. pp. 118-123.
  [ pdf / BibTeX ]
• "'Proof-Directed Debugging' Revisited for a First-Order Version."
  Kwangkeun Yi.
  Journal of Functional Programming. 2006.
  [ pdf / BibTeX ]
• "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. June 2005.
  [ pdf / BibTeX ]
• "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.
  Static Analysis: 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005. Proceedings. September 2005. pp. 203-217.
  [ ps.gz / BibTeX ]

Exception Analysis

Works on estimating uncaught exceptions in programs

• "Type and Effect System for Multi-Staged Exceptions."
  Hyunjun Eo and Ik-soon Kim and Kwangkeun Yi.
  4th Asian Symposium on Programming Languages and Systems. 2006. pp. 61-78.
  [ pdf / BibTeX ]
• "An Uncaught Exception Analysis for Java."
  Jangwoo Jo and Byeong-Mo Chang and Kwangkeun Yi and Kwang-Moo Choe.
  Journal of Systems and Software. 72 (1). 2004. pp. 59--69.
  [ ps.gz / BibTeX ]
• "A Cost-effective Estimation of Uncaught Exceptions in {SML} Programs."
  Kwangkeun Yi and Sukyoung Ryu.
  Theoretical Computer Science. 277 (1--2). April 2002. pp. 185--217.
  [ ps.gz / BibTeX ]
• "Exception Analysis for Multithreaded Java Programs."
  Sukyoung Ryu and Kwangkeun Yi.
  The Second Asia-Pacific Conference on Quality Software. December 2001.
  [ pdf / BibTeX ]
• "Interprocedural Exception Analysis for Java."
  Byeong-Mo Chang and Jangwoo Jo and Kwangkeun Yi and {Kwang-Moo} Choe.
  Proceedings of the 16th ACM Symposium on Applied Computing. March 2001.
  [ ps / BibTeX ]
• "Exception Analysis for Java."
  Kwangkeun Yi and Byeong-Mo Chang.
  Proceedings of ECOOP'99 Workshop on Formal Techniques for Java Programs. June 1999. pp. 111-112.
  [ ps / BibTeX ]
• "An Abstract Interpretation for Estimating Uncaught Exceptions in Standard ML Programs."
  Kwangkeun Yi.
  Science of Computer Programming. 31 (1). 1998. pp. 147--173.
  [ ps / BibTeX ]
• "Towards A Cost-Effective Estimation of Uncaught Exceptions in SML Programs."
  Kwangkeun Yi and Sukyoung Ryu.
  Proceedings of the Annual International Static Analysis Symposium. Paris, France. September 1997. pp. 98--113.
  [ ps.gz / slide.ps.gz / BibTeX ]
• "Estimating Uncaught Exceptions in Standard ML Programs from Type-based Equations."
  Kwangkeun Yi and Sukyoung Ryu and Ki-Hyun Pyun.
  The 20th Annual International Computer Software and Applications Conference. Seoul, Korea. August 1996. pp. 455--460.
  [ ps.gz / BibTeX ]
• "Compile-time Detection of Uncaught Exceptions in Standard ML Programs."
  Kwangkeun Yi.
  The 1st International Static Analysis Symposium. Namur. September 1994. pp. 238--254.
  [ ps.gz / BibTeX ]

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."
  Oukseh Lee, Hongseok Yang and Kwangkeun Yi.
  ESOP 2005: The European Symposium on Programming. 2005. pp. 124-140.
  [ pdf / BibTeX ]
• "Static Insertion of Safe and Effective Memory Reuse Commands into ML-like Programs."
  Oukseh Lee and Hongseok Yang and Kwangkeun Yi.
  Science of Computer Programming. 58 (1-2). 2005. pp. 141-178.
  [ pdf / BibTeX ]
• "Experiments on the Effectiveness of an Automatic Insertion of Safe Memory Reuses into ML-like Programs."
  Oukseh Lee and Kwangkeun Yi.
  Informal Proceedings of 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management. Venice, Italy. January 2004.
  [ pdf / slide.ppt / BibTeX ]
• "Inserting Safe Memory Reuse Commands into ML-like Programs."
  Oukseh Lee and Hongseok Yang and Kwangkeun Yi.
  Proceedings of the Annual International Static Analysis Symposium. San Diego, California. June 2003. pp. 171--188.
  [ pdf / BibTeX ]

Program Analysis Tools

Works on automatic generations and management of program analyses

• "Sound Non-Statistical Clustering of Static Analysis Alarms."
  Woosuk Lee and Wonchan Lee and Kwangkeun Yi.
  VMCAI 2012: 13th International Conference on Verification, Model Checking, and Abstract Interpretation. 2012.
  [ pdf / BibTeX ]
• "MeCC: Memory Comparison-based Clone Detector."
  Heejung Kim and Yungbum Jung and Sunghun Kim and Kwangkeun Yi.
  Proceedings of The International Conference on Software Engineering. 2011. pp. 301-310.
  [ pdf / BibTeX ]
• "An Algorithmic Mitigation of Large Spurious Interprocedural Cycles in Static Analysis."
  Hakjoo Oh and Kwangkeun Yi.
  Software - Practice and Experience. 40 (8). 2010. pp. 585--603.
  [ pdf / BibTeX ]
• "PCC Framework for Program-Generators."
  Soonho Kong and Wontae Choi and Kwangkeun Yi.
  Workshop on Proof-Carrying Code and Software Certification. 2009.
  [ pdf / BibTeX ]
• "Goal-directed Weakening of Abstract Interpretation Results."
  Hongseok Yang and Sunae Seo and Kwangkeun Yi and Taisook Han.
  ACM Transactions on Programming Langauges and Systems. 29 (6). 2007. pp. Article No.39.
  [ pdf / BibTeX ]
• "Static Monotonicity Analysis for Lambda-definable Functions over Lattices."
  Andrzej Murawski and Kwangkeun Yi.
  Third International Workshop on Verification, Model Checking and Abstract Interpretation. Venice, Italy. January 2002.
  [ pdf / BibTeX ]
• "{SUIF} Program Analysis Using System Z2."
  Seong-Hoon Kim and Kwangkeun Yi and Hyun-jun Eo and Kwang-Moo Choe.
  Proceedings of The Second SUIF Compiler Workshop. August 1997.
  [ ps.gz / BibTeX ]
• "Efficient computation of fixpoints that arise in complex program analysis."
  Liling Chen and Luddy Harrison and Kwangkeun Yi.
  Journal of Programming Languages. 3 (1). 1995. pp. 31--68.
  [ ps.gz / BibTeX ]
• "Automatic Generation and Management of Interprocedural Program Analyses."
  Kwangkeun Yi and Williams Ludwell {Harrison III}.
  Proceedings of ACM Symposium on Principles of Programming Languages. January 1993. pp. 246--259.
  [ ps.gz / BibTeX ]
• "Automatic Generation and Management of Program Analyses."
  Kwangkeun Yi.
  University of Illinois at Urbana-Champaign. 1993.
  [ ps.gz / BibTeX ]

Program Logics

Works on algorithmic aspects of program logics and model checking

• "GMeta: A Generic Formal Metatheory Framework for First-Order Representation."
  Gyesik Lee and Bruno Oliveira and Sungkeun Cho and Kwangkeun Yi.
  ESOP 2012: The European Symposium on Programming. 2012.
  [ pdf / BibTeX ]
• "The Implicit Calculus: A New Foundation for Generic Programming."
  Bruno C. d. S. Oliveira and Tom Schrijvers and Wontae Choi and Wonchan Lee and Kwangkeun Yi.
  PLDI 2012: 33rd ACM Conference on Programming Language Design and Implementation. 2012.
  [ pdf / BibTeX ]
• "How to find a coin: propositional program logics made easy."
  Logic in Computer Science. Nikolay V. Shilov and Kwangkeun Yi.
  World Scientific. Current Trends in Theoretical Computer Science. vol. 2: Formal Models and Semantics. April 2004. pp. 181--214.
  [ ps.gz / BibTeX ]
• "A Note on Model Checking Reuse."
  Nikolay Shilov and Kwangkeun Yi.
  2nd Australian Workshop on Computational Logic. Gold Cost, Australia. January 2001.
  [ ps.gz / BibTeX ]
• "How to Find a Coin: Propositional Program Logics Made Easy."
  Nikolay Shilov and Kwangkeun Yi.
  Bulletin of the European Association for Theoretical Computer Science. vol. 75. 2001. pp. 127-151.
  [ ps / BibTeX ]
• "On Expressive Power of Second Order Propositional Program Logics."
  Nikolay Shilov and Kwangkeun Yi.
  A. Ershov 4th International Conference on Perspectives of System Informatics. Novosibrisk, Russia. July 2001.
  [ ps.gz / BibTeX ]
• "On Expressive and Model Checking Power of Propositional Program Logics."
  Nikolay Shilove and Kwangkeun Yi.
  Perspectives of System Informatics: 4th International Andrei Ershov Memorial Conference. 2001. pp. 39-46.
  [ ps / BibTeX ]
• "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.
  [ pdf / BibTeX ]
• "A New Proof of Exponential Decidability for Propositional Mu-Calculus with Program Converse."
  Nikolay Shilov and Kwangkeun Yi.
  {III} International Conference on Theoretical Aspects of Computer Science. Novi Sad, Yugoslavia. September 2000.
  [ ps.gz / BibTeX ]
• "Model Checking Puzzles in Mu-Calculus."
  Nikolay Shilov and Kwangkeun Yi.
  Joint Bulletin of the Novosibirsk Computing Center and A.P.Ershov Institute of Informatics Systems. no. 13, . 2000.
  [ ps.gz / BibTeX ]
• "Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles for Testing Model Checkers."
  Nikolay Shilov and Kwangkeun Yi.
  Formal Methods Elsewhere. Pisa, Italy. October 2000.
  [ ps.gz / BibTeX ]

Program Transformation

Works on program transformations

• "Interconnecting Between CPS Terms and Non-CPS Terms."
  Jung-taek Kim and Kwangkeun Yi.
  The Proceedings of the Third ACM SIGPLAN Workshop on Continuations (CW'01). 2001. pp. 7-16.
  [ ps.gz / BibTeX ]
• "Interconnecting Between {CPS} Terms and Non-{CPS} Terms."
  Jung-taek Kim and Kwangkeun Yi.
  The Third ACM SIGPLAN Workshop on Continuations. London. January 2001.
  [ ps.gz / BibTeX ]
• "Assessing the Overhead of ML Exceptions by Selective CPS Transformation."
  Jung-taek Kim and Kwangkeun Yi and Olivier Danvy.
  The 1998 ACM SIGPLAN Workshop on ML. Baltimore. September 1998. pp. 103--114.
  [ ps / BibTeX ]

Separation Logic

Works on reasoning about pointers

• "Separation and Information Hiding."
  Peter W. O'Hearn and John C. Reynolds and Hongseok Yang.
  Proceedings of ACM Symposium on Principles of Programming Languages. January 2004. pp. 268--280.
  [ ps / BibTeX ]
• "A Semantic Basis for Local Reasoning."
  Hongseok Yang and Peter W. O'Hearn.
  Foundataions of Software Science and Computation Structures. Grenoble, France. April 2002.
  [ ps.gz / pdf / BibTeX ]
• "Computability and Complexity Results for a Spatial Assertion Language for Data Structures."
  Cristiano Calcagno and Hongseok Yang and Peter W. O'Hearn.
  Foundations of Software Technology and Theoretical Computer Science. Bangalore, India. December 2001.
  [ ps.gz / pdf / BibTeX ]
• "Correctness of Data Representations involving Heap Data Structures."
  Uday S. Reddy and Hongseok Yang.
  Science of Computer Programming.
  [ ps / BibTeX ]
• "Possible Worlds and Resources: The Semantics of BI."
  Peter W. O'Hearn and David Pym and Hongseok Yang.
  Theoretical Computer Science.
  [ ps.gz / BibTeX ]

Staged Programming Languages

• "Static Analysis of Multi-Staged Programs via Unstaging Translation."
  Wontae Choi and Baris Aktemur and Kwangkeun Yi and Makoto Tatsuda.
  Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2011. pp. 81--92.
  [ pdf / BibTeX ]
• "Abstract parsing for two-staged languages with concatenation."
  Soonho Kong and Wontae Choi and Kwangkeun Yi.
  Proceedings of the 8th International Conference on Generative Programming and Component Engineering (GPCE'09). 2009. pp. 109--116.
  [ pdf / BibTeX ]
• "A Polymorphic Modal Type System for Lisp-Like Multi-Staged Languages."
  Ik-Soon Kim and Kwangkeun Yi and Cristiano Calcagno.
  Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2006. pp. 257--269.
  [ pdf / BibTeX ]

Syntactic Analysis

Works on syntactic analyses of program texts.

• "LR Error Repair Using the A* Algorithm."
  Ik-Soon Kim and Kwangkeun Yi.
  Acta Informatica. 47 (3). 2010. pp. 179--207.
  [ pdf / BibTeX ]

Type Systems

Works on type systems and their algorithms

• "Proofs of a Set of Hybrid Let-Polymorphic Type Inference Algorithms."
  Hyunjun Eo and Oukseh Lee and Kwangkeun Yi.
  New Generation Computing. 22 (1). November 2003. pp. 1--36.
  [ BibTeX ]
• "Proofs about a Folklore Let-Polymorphic Type Inference Algorithm."
  Oukseh Lee and Kwangkeun Yi.
  ACM Transactions on Programming Languages and Systems. 20 (4). July 1998. pp. 707--723.
  [ pdf / BibTeX ]

Other Program Analyses

• "Predicate Generation for Learning-Based Quantifier-free Loop Invariant Inference."
  Yungbum Jung and Wonchan Lee and Bow-Yaw Wang and Kwangkeun Yi.
  TACAS 2011: 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2011. pp. 205--219.
  [ pdf / BibTeX ]
• "Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates."
  Soonho Kong and Yungbum Jung and Cristina David and Bow-Yaw Wang and Kwangkeun Yi.
  APLAS 2010: 8th Asian Symposium on Programming Languages and Systems. 2010. pp. 328--343.
  [ pdf / BibTeX ]
• "Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction."
  Yungbum Jung and Soonho Kong and Bow-Yaw Wang and Kwangkeun Yi.
  VMCAI'10: Proceeding of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation. 2010. pp. 180-196.
  [ pdf / BibTeX ]
• "Static Extensivity Analysis for Lambda-definable Functions over Lattices."
  Hyunjun Eo and Kwangkeun Yi and Kwangmoo Choe.
  New Generation Computing. 24 (1). 2006. pp. 53-78.
  [ ps / BibTeX ]
• "Automatic Construction of Hoare Proofs from Abstract Interpretation Results."
  Sunae Seo and Hongseok Yang and Kwangkeun Yi.
  Proceedings of the 1st Asian Symposium on Programming Languages and Systems. 2003. pp. 230--245.
  [ pdf / BibTeX ]
• "A Proof Method for the Correctness of Modularized {0CFA}."
  Oukseh Lee and Kwangkeun Yi and Yunheung Paek.
  Information Processing Letters. 81 (4). February 2002. pp. 179--185.
  [ pdf / BibTeX ]
• "Engaging Students with Theory through ACM Collegiate Programming Contests."
  Nikolay Shilov and Kwangkeun Yi.
  Communications of the ACM. 45 (9). September 2002. pp. 98--101.
  [ ps.gz / BibTeX ]
• "Proving Syntactic Properties of Exceptions in an Ordered Logical Framework."
  Jeff Polakow and Kwangkeun Yi.
  The Fifth International Symposium on Functional and Logic Programming. Tokyo, Japan. March 2001. pp. 61--77.
  [ ps.gz / BibTeX ]
• "Unified Interprocedural Parallelism Detection."
  Jay Hoeflinger and Yunheung Paek and Kwangkeun Yi.
  International Journal of Parallel Programming. 29 (2). April 2001. pp. 185--215.
  [ ps.gz / BibTeX ]
• "Constraint-based Analysis for Java."
  Byeong-Mo Chang and Kwangkeun Yi and Jangwoo Jo.
  SSGRR Conference on Computers and E-Business. L'Aquila, Italy. August 2000.
  [ ps.gz / BibTeX ]
• "Escape Analysis for Stack Allocation in Java."
  Eunsun Cho and Kwangkeun Yi.
  ECOOP Workshop on Formal Techniques for Java Programs. Canne, France. June 2000.
  [ ps.gz / BibTeX ]