Kyungmin Bae

Education

Research Interests

• Formal Method and Model Checking
• Program Analysis and Software Verification
• High-order and Meta Programming
• Logic and Applied Mathematics

Publication

Abstract Logical Model Checking of Infinite-State Systems Using Narrowing, Kyungmin Bae, Santiago Escobar and Jose Meseguer, International Conference on Rewriting Techniques and Applications (RTA), 2013 (To appear)

PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude, Kyungmin Bae, Josh Krisiloff, Jose Meseguer, and Peter Olveczky, International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), 2012

Formal Patterns for Multi-Rate Distributed Real-Time Systems, Kyungmin Bae, Jose Meseguer, and Peter Olveczky, International Symposium on Formal Aspects of Component Software (FACS), 2012

Model Checking LTLR Formulas under Localized Fairness, Kyungmin Bae and Jose Meseguer, 9th International Workshop on Rewriting Logic and its Applications, 2012

The SynchAADL2Maude Tool, Kyungmin Bae, Peter Olveczky, Jose Meseguer, and Abdullah Al-Nayeem, International Conference on Fundamental Approaches to Software Engineering (FASE), 2012

Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude, Kyungmin Bae, Peter C. Olveczky, Thomas H. Feng, Edward A. Lee and Stavros Tripakis, Science of Computer Programming 77(12), 2012

Synchronous AADL and its Formal Analysis in Real-Time Maude, Kyungmin Bae, Peter Olveczky, Abdullah Al-Nayeem and Jose Meseguer, International Conference on Formal Engineering Methods (ICFEM), Oct, 2011

State/Event-based LTL Model Checking under Parametric Generalized Fairness, Kyungmin Bae and Jose Meseguer, Computer Aided Verification (CAV), July, 2011

Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models, Kyungmin Bae and Peter C. Olveczky, 1st International Workshop on Rewriting Techniques for Real-Time Systems, April 7, 2010

The Linear Temporal Logic of Rewriting Maude Model Checker, Kyungmin Bae and Jose Meseguer, 8th International Workshop on Rewriting Logic and its Applications, Mar 20, 2010

Verifying Ptolemy II Discrete-Event Models using Real-Time Maude, Kyungmin Bae, Peter C. Olveczky, Thomas H. Feng and Stavros Tripakis, International Conference on Formal Engineering Methods (ICFEM), Dec 8, 2009

A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting, Kyungmin Bae and Jose Meseguer, 9th International Workshop on Rule-Based Programming, July 18, 2008

Projects

• Maude LTLR Model Checker
• SynchAADL2Maude tool
• Maude LTL LMC Model Checker

Research Experience

Research Assistant, Department of Computer Science, UIUC, 2008 - present

• Synchronous AADL model verification using the Real-Time Maude system
• Ptolemy II verification in NAOMI (New Associative Object Model of Integration) Project
• Meta-level based theorem transformation for state/event model checking in Maude (link)

International Fellow, CSL, SRI International, May 2009 ~ Aug 2009

• Developed the Maude Linear Temporal Logic of Rewriting Model Checker

Research Assistant, Programming Research Laboratory, KAIST, 2003

• Abstract interpretation based program analysis