Kyungmin Bae

Education

Research Interests

• Formal Methods and Model Checking
• Algebraic Specification and Rewriting Logic
• Program Analysis and Software Verification
• Logic and Applied Mathematics

Conference Publication

Predicate Abstraction of Rewrite Theories, Kyungmin Bae and Jose Meseguer, Rewriting Techniques and Applications (RTA), 2014

Definition, Semantics, and Analysis of Multirate Synchronous AADL, Kyungmin Bae, Peter Olveczky, and Jose Meseguer, International Symposium on Formal Methods (FM), 2014

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

The SynchAADL2Maude Tool, Kyungmin Bae, Peter Olveczky, Jose Meseguer, and Abdullah Al-Nayeem, International Conference on Fundamental Approaches to Software Engineering (FASE), 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

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

Journal Publication

Designing and Verifying Distributed Cyber-Physical Systems using Multirate PALS: An Airplane Turning Control System Case Study, Kyungmin Bae, Josh Krisiloff, Jose Meseguer, and Peter Olveczky, Science of Computer Programming, 2014 (To appear)

Model Checking Linear Temporal Logic of Rewriting Formulas under Localized Fairness, Kyungmin Bae, and Jose Meseguer, Science of Computer Programming, 2014 (in press, http://dx.doi.org/10.1016/j.scico.2014.02.006)

Formal Patterns for Multirate Distributed Real-Time Systems (extended version), Kyungmin Bae, Jose Meseguer, and Peter Olveczky, Science of Computer Programming 91, Part A, 2014

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

Workshop Publication

Infinite-State Model Checking of LTLR Formulas Unsing Narrowing, Kyungmin Bae and Jose Meseguer, 10th International Workshop on Rewriting Logic and its Applications, 2014 (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

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

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 - 2014

• Synchronous AADL model verification using the Real-Time Maude system (link)
• Ptolemy II verification in NAOMI (New Associative Object Model of Integration) Project

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

• Developed the Maude Linear Temporal Logic of Rewriting Model Checker