Moonzoo Kim's Home Page

Last update: Sep 8, 2006

resume

Contact Information

Rm# 2434, CS Dept. KAIST
373-1 Guseong-dong, Yuseong-gu
Daejeon 305-701 Republic of Korea
TEL: +82-42-869-3543
FAX: +82-42-869-3510
mailto:moonzoo [at] cs.kaist.ac.kr

Background

  • Sep 2006 - present: Assistant Professor at CS dept. KAIST, leading
  • 2004 - Aug 2006: Researcher at Pohang University of Science and Technology
  • 2002 - 2004: Research Engineer at Samsung SECUi.COM
  • 1997 - 2001: Ph.D degree in CIS, Univ. of of Pennsylvania
    Dissertation: Information extraction for run-time formal analysis (slides)
    Advisor: Sampath Kannan and Insup Lee
  • 1995 - 1997: MS degree in Computer and Information Science, University of Pennsylvania
  • 1992 - 1995: B.S. degree in Computer Science, Korea Advanced Institute of Science and Technology
  • 1990 - 1992: Seoul Science High School

    Research Interests

  • Formal Methods
    - Runtime Verification
     - Model Checking
  • Software Engineering
    - Automated software analysis
    - Reverse-engineering/re-engineering
  • Real-time Embedded Systems
    - Formal techniques for modelling, design, and testing

    Teaching

  • Fall 2006, CS750B Software Model Checking
  • Spring 2007, CS550 Introduction to Software Engineering

    • Publications

    International Journals

  • Foundations for Monitoring and Checking Reactive Systems
    M.Viswanathan and M.Kim
    Submitted to Springer Formal Aspects of Computing
  • Using Formal Modelling with an Automated Analysis Tool to Design and Parametrically Analyze a Multi-robot Coordination Protocol: a case study
    J. Esposito and M. Kim
    To appear at IEEE Transactions on Systems, Man, and Cybernetics, Part A
  • Java-MaC: a Rigorous Run-time Assurance Tool for Java Programs
    M. Kim, S. Kannan, I. Lee, O. Sokolsky, and M. Viswanathan
    Formal Methods in System Design, 2004 (vol 24 no 2)
  • Verisim: Formal Analysis of Network Simulations
    K.Bhargavan, C.A.Gunter, M.Kim, I.Lee, D.Obradovic, O.Sokolsky, and M.Viswanathan
    IEEE Transaction of Software Engineering (vol 28 no 2)

    International Conferences

    2002 - present
  • Re-engineering a Credit Card Authorization System for Maintainability and Re-usability of Components: a Case Study
    K.C.Kang, J.Lee, B. Kim, M.Kim, C. Seo, and S. Yu
    International Conference on Software Reuse, Torino, Italy, 2006 (LNCS 4039)
  • Formal Construction and Verification of Home Service Robots: A Case Study (slides)
    M. Kim and K.C.Kang
    Automated Technology for Verification and Analysis, Taiwan, Taipei, Oct 2005 (LNCS 3707)
  • Feature-oriented Re-engineering of Legacy Systems into Product Line Assets: A Case Study
    K.C.Kang, M. Kim, J. Lee, and B. Kim
    International Software Product Line Conference, Rennes, France, Sep 2005 (LNCS 3714)
  • Re-engineering Software Architecture of Home Service Robots: A Case Study (slides)
    M. Kim, J. Lee, K.C.Kang, Y. Hong, and S. Bang
    IEEE International Conference on Software Engineering, St. Louis Missouri, USA, May 2005
  • 3D Virtual Prototyping of Home Service Robots Using ASADAL/OBJ (slides)
    K.C.Kang, M. Kim, J. Lee, B. Kim, Y. Hong, H. Lee, and S. Bang
    IEEE International Conference on Robotics and Automation, Barcelona, Spain, April 2005
  • Formal Verification of the Robot Movements- a Case Study on Home Service Robot SHR100 (slides)
    M. Kim, K.C.Kang, and H. Lee
    International Conference on Robotics and Automation, Barcelona, Spain, April 2005
  • Foundations for the Run-time Monitoring of Reactive Systems: Fundamentals of the MaC Language (slides)
    M. Viswanathan and M. Kim
    International Colloquium on Theoretical Aspects of Computing, Guiyang, China Sep 2004 (LNCS 3407)
  • Computational Analysis of Run-time Monitoring – Fundamentals of Java-MaC (slides)
    M. Kim, S. Kannan, I. Lee, O. Sokolsky, and M. Viswanathan
    Runtime Verification, Copenhagen Denmark July 2002 (ENTCS vol 70 no 4)
  • Monitoring, Checking, and Steering of Real-time Systems
    I.Lee, U. Sammapun, J. Shin, and O. Sokolsky
    Runtime Verification, Copenhagen Denmark July 2002 (ENTCS vol 70 no 4)

    Before 2002 (i.e. works done at U.Penn)
  • Java-MaC: a Run-time Assurance Tool for Java Programs
    M. Kim, S. Kannan, I. Lee, O. Sokolsky, and M. Viswanathan
    Runtime Verification Paris France July 2001 (ENTCS vol 55 no 2)
  • Verisim: Formal Analysis of Network Simulations
    K. Bhargavan, C.A. Gunter, M. Kim, I. Lee, D. Obradovic, O. Sokolsky, and M. Viswanathan
    Proceedings of the International Symposium on Software Testing and Analysis, August 2000
  • Formal Modelling and Analysis of Hybrid Systems: A Case Study in Multirobot Coordination
    R.Alur, J. Esposito, M.Kim, V.Kumar and I. Lee
    FM'99 World Congress On Formal Methods In The Development Of Computing Systems Sep 20-24,1999, Toulouse, France (LNCS 1708)
  • Runtime Assurance Based On Formal Specifications
    Insup Lee, S. Kannan,  M. Kim, O. Sokolsky, M. Viswanathan
    999 International Conference on Parallel and Distributed Processing Techniques and Applications, June 28 - July 1, 1999, Monte Carlo Resort, Las Vegas,Nevada, USA
  • Formally Specified Monitoring of Temporal Properties
    Moonjoo Kim, Mahesh Viswanathan, Hanene Ben-Abdallah, Sampath Kannan, Insup Lee and Oleg Sokolsky
    European Conference on Real-Time Systems, York, UK June 9-11, 1999
  • Steering of Real-Time Systems based on Monitoring and Checking
    O. Sokolsky, S. Kannan, M. Kim, I.Lee and M.Viswanathan
    Fourth International Workshop on Object-Oriented Real-time Dependable Systems, January 27-29, 1999 Santa Barbara, California, USA
  • A Monitoring and Checking Framework for Run-time Correctness Assurance
    Insup Lee, H. Ben-Abdallah, S. Kannan, M. Kim, O. Sokolsky, M. Viswanathan
    Proc. 1998 Korea-U.S. Technical Conference on Strategic Technologies, Vienna, VA , Oct 22-24, 1998

    Words from the Bible

  • Jesus replied, "You must love the Lord your God with all your heart, all your soul, and all your mind". This is the first and greatest commandment. A second is equally important:"Love your neighbor as yourself". All the other commandments and all the demands of the prophets are based on these two commandments... Matthew 23:37-40

  • But he said to me "My grace is sufficient for you, for my power is made perfect in weakness". Therefore I will boast all the more gladly about my weaknesses, so that Christ's power may rest on me. That's why, for Christ's sake, I delight in weaknesses, in insults, in hardships, in persecutions, in difficulties. For when I am weak, then I am strong....2Corinthians 12:9-10

  • Through love and faithfulness sin is atoned for, through the fear of the LORD a man avoids evil... Proverb 16:6

  • We are made right in God's sight when we trust in Jesus Christ to take away our sins. And we all can be saved in this same way, no matter who we are or what we have done ... Roman 3:22

  • Love is patient, love is kind. It does not envy, it does not boast, it is not proud. It is not rude, it is not self-seeking, it is not easily angered, it keeps no record of wrongs. Love does not delight in evil but rejoices with the truth. It always protects, always trusts, always hopes, always perseveres... 1Cor 13:4 - 7

    If you have time...

    Vi joke of the millennium:

    (user) I'm having trouble with this editor
    (admin) Which one are you using ?
    (user) Um, I dunno.
    (admin) Emacs? Which version are you running ?
    (user) Umm, I'm running version vi, and having heaps of trouble. Is vii out?
    (admin) Say what?
    (user) Have they done anything new?
    (admin) Well... Yeah, they're up to xv now, but that needs a special graphical interface.
    (user) Oh, well, thanks anyway.
    (admin) *shudder*

    Etc

  • Four Spiritual Laws

  • I start using moonzoo as my first name since 2004 due to pronunciation problem for 'j' in moonjoo ('j' is pronounced as 'j', 'h', or 'y' in different languages).