Please visit the following original sites: (updated on Dec 2015)
Books

  1. S.Cha, J.Y.Choi, M.Kim, I.Lee, M.Viswanathan (Eds.), Proceeding of 6th International Symposium of Automated Technology for Verification and Analysis (LNCS5311), Seoul, Korea, October 20-23, 2008 [BibTeX]

International Journals

  1. S. Hong, M. Staats, J. Ahn, M. Kim, G. Rothermel, Are Concurrency Coverage Metrics Effective for Testing: A Comprehensive Empirical InvestigationJournal of Software Testing, Verification and Reliability (STVR), volume 25, issue 4, pages 334-370, June 2015
  2. S. Hong and M. Kim, A survey of race bug detection techniques for multithreaded programsJournal of Software Testing, Verification and Reliability (STVR), volume 25, issue 3, pages 191-217, May 2015
  3. Z. Xu, Y. Kim, M. Kim, M. Cohen, and G. Rothermel, Directed Test Suite Augmentation: An Empirical InvestigationJournal of Software Testing, Verification and Reliability (STVR), volume 25, issue 2, pages 77-114, March 2015
  4. Y.Kim, O.Choi, M.Kim, J.Baik, and T.Kim, Validating Software Reliability Early through Statistical Model CheckingIEEE Software, pages 35-41, vol 30, issue 3, May/June 2013
  5. S. Hong and M. Kim, Effective Pattern-driven Concurrency Bug Detection for Operating SystemsJournal of Systems and Software (JSS), vol 86, issue 2, pages 377–388, Feb 2013
  6. M.Kim, Y.Kim and Y.Choi, Concolic Testing of the Multi-sector Read Operation for Flash Storage Platform SoftwareFormal Aspects of Computing (FACJ), vol 24, no 2, pp 355-374, May 2012 [BibTeX]
  7. Y.Choi and M.Kim, Controlled Composition and Abstraction for Bottom-up Integration and Verification of Abstract ComponentsInformation and Software Technology (IST), vol 54, issue 1, page 119-136, Jan 2012 [BibTeX]
  8. M.Kim, Y.Kim, and H.Kim, A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case StudyIEEE Transactions on Software Engineering (TSE), vol 37, no 2, pages 146-160, March 2011 [BibTeX]
  9. J.Esposito and M.Kim, Using Formal Modeling with an Automated Analysis Tool to Design and Parametrically Analyze a Multi-robot Coordination Protocol: a case studyIEEE Transactions on Systems, Man, and Cybernetics (SMC) Part A, vol 37, no.3, pages 285-297, May 2007 [BibTeX]
  10. M.Kim, S.Kannan, I.Lee, O.Sokolsky, and M.Viswanathan, Java-MaC: A Run-Time Assurance Approach for Java ProgramsFormal Methods in System Design (FMSD), vol 24, no 2, pages 129-155, Mar 2004 [BibTeX]
  11. K.Bhargavan, C.A.Gunter, M.Kim, I.Lee, D.Obradovic, O.Sokolsky, and M.Viswanathan, Verisim: Formal Analysis of Network Simulations,IEEE Transactions on Software Engineering (TSE), vol 28, no 2, pages 129-145, Feb 2002 [BibTeX]

International Conferences and Workshops

2015:

  1. S. Hong, B. Lee, T. Kwak, Y. Jeon, B. Ko, Y. Kim, and M. Kim, Mutation-based Fault Localization for Real-world Multilingual Programs,IEEE/ACM International Conference on Automated Software Engineering (ASE), Nov 9-13, 2015 (acceptance rate:19%)
  2. Y. Park, S. Hong, M. Kim, D. Lee, and J. Cho, Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric OvenIntl. Conf. on Software Engineering (ICSE) Software Engineering In Practice (SEIP) track, May 2015 (acceptance rate:23%)

2014:

  1. Y. Kim and M. Kim, SAT-based Bounded Software Model Checking for Embedded Software: A Case StudyAsia-Pacific Software Engineering Conference (APSEC), Dec 1-4 2014
  2. S.Moon, Y.Kim, M.Kim, S.Yoo, Ask the Mutants: Mutating Faulty Programs for Fault LocalizationIEEE International Conference on Software Testing, Verification and Validation (ICST), March 31-April 4, 2014 [tech. report and pptx slides w/ the revised suspiciousness metric and the extended experiment results] 
  3. S. Hong, Y. Park, M. Kim, Detecting Concurrency Errors in Client-side JavaScript Web ApplicationsIEEE International Conference on Software Testing, Verification and Validation (ICST), March 31-April 4, 2014 
  4. Y.Kim, Z.Xu, M.Kim, M.Cohen, and G.Rothermel, Hybrid Directed Test Suite Augmentation: An Interleaving FrameworkIEEE International Conference on Software Testing, Verification and Validation (ICST), March 31-April 4, 2014 

2013:

  1. Y.Kim, Y.Kim, T.Kim, G.Lee, Y.Jang, and M.Kim, Automated Unit Testing of Large Industrial Embedded Software using Concolic TestingIEEE/ACM Automated Software Engineering (ASE) Experience track, Nov 11-15, 2013 (acceptance rate:23%)
  2. S. Hong, M. Staats, J. Ahn, M. Kim, and G. Rothermel, The Impact of Concurrent Coverage Metrics on Testing EffectivenessIEEE International Conference on Software Testing, Verification and Validation (ICST), Mar 18-22, 2013 (acceptance rate:25%)

2012:

  1. Y.J.Kim and M.Kim, Hybrid Statistical Model Checking Technique for Reliable Safety Critical Systems,  IEEE Intl. Symp. on Software Reliability Engineering (ISSRE), Dallas, TX USA, Nov 27-30, 2012
  2. Y.J.Kim, M.Kim, and T.Kim,  Statistical Model Checking for Safety Critical Hybrid Systems: An Empirical EvaluationHaifa Verification Conference (HVC), Haifa, Israel, Nov 6-8, 2012
  3. M. Staats, S. Hong, M. Kim, and G. Rothermel, Understanding User Understanding: Determining Correctness of Generated Program InvariantsIntl. Symp. on Software Testing and Analysis (ISSTA), 2012
  4. S. Hong, J. Ahn, S. Park, M. Kim, and M. J. Harrold, Testing Concurrent Programs to Achieve High Synchronization CoverageIntl. Symp. on Software Testing and Analysis (ISSTA), 2012
  5. Y.Kim, M.Kim, Y.J.Kim, and Y.Jang, Industrial Application of Concolic Testing Approach: A Case Study on libexif by Using CREST-BV and KLEEIntl. Conf. on Software Engineering (ICSE), Software Engineering in Practice (SEIP) track, June 2-9, 2012 (acceptance rate:19%)
  6. M.Kim, Y.Kim and G.Rothermel, A Scalable Distributed Concolic Testing Approach: An Empirical EvaluationIEEE International Conference on Software Testing, Verification and Validation (ICST), April 17-21, 2012
  7. M.Kim, Y.Kim and Y.Jang, Industrial Application of Concolic Testing on Embedded Software: Case StudiesIEEE International Conference on Software Testing, Verification and Validation (ICST) Industrial track, April 17-21, 2012, nominated as a best paper (acceptance rate: 23%)

2011:

  1. Z.Xu, Y.Kim, M.Kim and G.Rothermel, A Hybrid Directed Test Suite Augmentation TechniqueIEEE Intl. Symp. on Software Reliability Engineering (ISSRE), Hiroshima, Japan, Nov 29-Dec 2 2011 (acceptance rate: 25%) [BibTeX]
  2. M.Kim and Y.Kim, Automated Analysis of Industrial Embedded SoftwareAutomated Technology for Verification and Analysis (ATVA), Taipei, Taiwan, Oct 11-14 2011  (invited paper) [BibTeX] [invited talk slides]
  3. Y.Kim and M.Kim, SCORE: a Scalable Concolic Testing Tool for Reliable Embedded SoftwareACM SIGSOFT Foundation of Software Engineering (FSE) Tool demonstration track, pages 420-423, Szeged, Hungary, Sep 5-9 2011 (4 page short paper) [BibTeX]
  4. Y.Kim, M.Kim and Y.Jang, Concolic Testing on Embedded Software - Case Studies on Mobile Platform ProgramsACM SIGSOFT Foundation of Software Engineering (FSE) Industrial track, Szeged, Hungary, Sep 5-9 2011 (4 page short paper)

2010:

  1. Z.Xu, Y.Kim, M.Kim, G.Rothermel, and M.Cohen, Directed Test Suite Augmentation: Techniques and TradeoffsACM SIGSOFT Foundation of Software Engineering (FSE), pages 257-266, Santa Fe, New Mexico, USA, Nov 7-11 2010 (acceptance rate: 20%) [BibTeX]
  2. Y.Kim, M.Kim, N.Dang, Scalable Distributed Concolic Testing: a Case Study on a Flash Storage PlatformGrand Challenge in Verified Software Track @ Intl. Conf. on Theoretical Aspects of Computing (ICTAC) (LNCS 6255), pages 199-213, Natal, Brazil, Sep 1-3 2010 [BibTeX]

2009:

  1. M.Kim and Y.Kim, Concolic Testing of the Multi-sector Read Operation for Flash Memory File SystemGrand Challenge in Verified Software Track @ Brazilian Symposium on Formal Methods (SBMF), pages 251-265, Gramado, Brazil, Aug 19-21 2009 (LNCS 5902) [BibTeX]
  2. M.Kim, S.Hong, C.Hong and T.Kim, Model-based Kernel Testing for Concurrency Bugs through Counter Example Replay,  Model-based Testing (ENTCS vol 253, no 2), pages 21-36, York, UK, Mar 22 2009 [BibTeX]

2008:

  1. M.Kim, Y.Kim and H.Kim, Unit Testing of Flash Memory Device Driver through a SAT-based Model CheckerIEEE/ACM Automated Software Engineering (ASE), pages 198-207, L'Aquila, Italy, Sep 15-19 2008 (acceptance rate: 12%) [BibTeX]
  2. M.Kim, Y.Choi, Y.Kim and H. Kim, Formal Verification of a Flash Memory Device Driver - an Experience ReportSpin Workshop (LNCS 5156), pages 144-159, LA, USA, August 10-12 2008 [BibTeX]
  3. M.Kim, Y.Kim, Y.Choi, and H.Kim, Pre-testing Flash Device Driver through Model Checking TechniquesIEEE Intl. Conf. on Software Testing, Verification and Validation (ICST), pages 475-484,  Lillehammer, Norway, April 9-11 2008  (acceptance rate: 20%) [BibTeX]

2007 and before:

  1. M.Kim, Formal Modeling and Verification of High-Availability Protocol for Network Security AppliancesAutomated Technology for Verification and Analysis (ATVA) (LNCS 4762), pages 489-500, Tokyo, Japan, Oct 22-25 2007 (short paper) [BibTeX]
  2. K.C.Kang, J.Lee, B.Kim, M.Kim, C.Seo, and S.Yu, Re-engineering a Credit Card Authorization System for Maintainability and Re-usability of Components: a Case StudyIntl. Conf. on Software Reuse (ICSR)(LNCS 4039), pages 156-169, Turin, Italy, June 12-15 2006 [BibTeX]
  3. M.Kim and K.C.Kang, Formal Construction and Verification of Home Service Robots: A Case StudyAutomated Technology for Verification and Analysis (ATVA) (LNCS 3707), pages 429-443, Taiwan, Taipei, Oct 4-7 2005 [BibTeX]
  4. K.C.Kang, M.Kim, J.Lee, and B.Kim, Feature-oriented Re-engineering of Legacy Systems into Product Line Assets: A Case StudySoftware Product Line Conference (SPLC) (LNCS 3714), pages 45-56, Rennes, France, Sep 26-29 2005 [BibTeX]
  5. M.Kim, J.Lee, K.C.Kang, Y.Hong, and S.Bang, Re-engineering Software Architecture of Home Service Robots: A Case StudyIntl. Conf. on Software Engineering (ICSE) Experience reports track, pages 505-513, St. Louis Missouri, USA, May 15-21 2005 (acceptance rate:20%) [BibTeX]
  6. K.C.Kang, M.Kim, J.Lee, B.Kim, Y.Hong, H.Lee, and S.Bang, 3D Virtual Prototyping of Home Service Robots Using ASADAL/OBJIEEE Intl. Conf. on Robotics and Automation (ICRA), pages 2903-2908, Barcelona, Spain, April 18-22 2005 [BibTeX]
  7. M.Kim, K.C.Kang, and H.Lee, Formal Verification of Robot Movements-a Case Study on Home Service Robot SHR100IEEE Intl. Conf. on Robotics and Automation (ICRA), pages 4739-4744, Barcelona, Spain, April 18-22 2005 [BibTeX]
  8. M.Viswanathan and M.Kim, Foundations for the Run-time Monitoring of Reactive Systems: Fundamentals of the MaC LanguageIntl. Conf. on Theoretical Aspects of Computing (ICTAC) (LNCS 3407), pages 543-556, Guiyang, China Sep 20-24 2004 [BibTeX]
  9. M.Kim, S.Kannan, I.Lee, O.Sokolsky, and M.Viswanathan, Computational Analysis of Run-time Monitoring – Fundamentals of Java-MaCRuntime Verification (RV) (ENTCS vol 70 no 4), pages 80-94, Copenhagen, Denmark, July 26 2002 [BibTeX]
  10. M.Kim, I.Lee, U.Sammapun, J.Shin, and O.Sokolsky, Monitoring, Checking, and Steering of Real-time SystemsRuntime Verification (RV)(ENTCS vol 70 no 4), pages 95-111, Copenhagen, Denmark, July 26 2002 [BibTeX]
  11. M.Kim, S.Kannan, I.Lee, O.Sokolsky, and M.Viswanathan, Java-MaC: a Run-time Assurance Tool for Java ProgramsRuntime Verification (RV) (ENTCS vol 55 no 2), pages 218-235, Paris, France, July 23 2001 [BibTeX]
  12. K.Bhargavan, C.A.Gunter, M.Kim, I.Lee, D.Obradovic, O.Sokolsky, and M.Viswanathan, Verisim: Formal Analysis of Network Simulations,ACM Intl. Symp. on Software Testing and Analysis (ISSTA), pages 2-13, Portland, Oregon, USA, August 22-24 2000 (acceptance rate:23%) [BibTeX]
  13. S.Kannan, M.Kim, I.Lee, O.Sokolsky, and M.Viswanathan, Run-time monitoring and steering based on formal specificationsModeling Software System Structures in a Fastly Moving Scenario, pages 167-177, Santa Margherita Ligure, Italy, June 13-16 2000 (invited paper)[BibTeX]
  14. R.Alur, J.Esposito, M.Kim, V.Kumar and I.Lee, Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot CoordinationWorld Congress On Formal Methods (FM) (LNCS 1708), pages 212-232, Toulouse, France, Sep 20-24 1999 [BibTeX]
  15. I.Lee, S.Kannan,  M.Kim, O.Sokolsky, M.Viswanathan, Runtime Assurance Based On Formal SpecificationsParallel and Distributed Processing Techniques and Applications (PDPTA), pages 279-287, Monte Carlo Resort, Las Vegas, Nevada, USA, June 28 - July 1, 1999 [BibTeX]
  16. M.Kim, M.Viswanathan, H.B.Abdallah, S.Kannan, I.Lee and O.Sokolsky, Formally Specified Monitoring of Temporal PropertiesEuropean Conference on Real-Time Systems (ECRTS), pages 114-122, York, UK, June 9-11, 1999 [BibTeX]
  17. O.Sokolsky, S.Kannan, M.Kim, I.Lee and M.Viswanathan , Steering of Real-Time Systems based on Monitoring and CheckingFourth International Workshop on Object-Oriented Real-time Dependable Systems, pages 11-18, Santa Barbara, California, USA, Jan 27-29, 1999 [BibTeX]
  18. I.Lee, H.Ben-Abdallah, S.Kannan, M.Kim, O.Sokolsky, M.Viswanathan, A monitoring and checking framework for run-time correctness assurance, Korea-U.S. Technical Conference on Strategic Technologies,Vienna, VA, October 1998.