Kyungmin Bae

Associate Professor
Department of Computer Science and Engineering
POSTECH (Pohang University of Science and Technology)

Email
kmbae at postech.ac.kr
Office
B2 225
Phone
+82-54-279-2256
Address
77 Cheongam-Ro, Nam-Gu, Pohang, Gyeongbuk, Korea 37673
Menu

About

I am an associate professor in the Department of Computer Science and Engineering at POSTECH, and lead the Software Verification Laboratory. I study automatic formal analysis and software engineering methods to develop safe and reliable computer systems.

Research Interests

Professional Activities

Software

Teaching

Publications

Conference Papers

  1. An Extension of HybridSynchAADL and Its Application to Collaborating Autonomous UAVs Jaehun Lee, Kyungmin Bae and Peter Olveczky International Symposium on Leveraging Applications of Formal Methods (ISoLA) 2022
  2. STLmc: Robust STL Model Checking of Hybrid Systems using SMT Geunyeol Yu, Jia Lee, and Kyungmin Bae International Conference on Computer Aided Verification (CAV) 2022
  3. Efficient SMT-Based Model Checking for Signal Temporal Logic Jia Lee, Geunyeol Yu, and Kyungmin Bae IEEE/ACM International Conference on Automated Software Engineering (ASE) 2021
  4. MSYNC: A Generalized Formal Design Pattern for Virtually Synchronous Multirate Cyber-Physical Systems Kyungmin Bae and Peter Olveczky International Conference on Embedded Software (EMSOFT) 2021
  5. HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL Jaehun Lee, Sharon Kim, Kyungmin Bae and Peter Olveczky International Conference on Computer Aided Verification (CAV) 2021
  6. Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation Kyungmin Bae and Jia Lee ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) 2019
  7. Modular SMT-Based Analysis of Nonlinear Hybrid Systems Kyungmin Bae and Sicun Gao International Conference on Formal Methods in Computer-Aided Design (FMCAD) 2017
  8. Guarded Terms for Rewriting modulo SMT Kyungmin Bae and Camilo Rocha International Conference on Formal Aspects of Component Software (FACS) 2017
  9. SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems Kyungmin Bae, Peter Olveczky, Soonho Kong, Sicun Gao, and Edmund M. Clarke ACM International Conference on Hybrid Systems: Computation and Control (HSCC) 2016
  10. A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control Robert P. Goldman, Daniel Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae International Symposium on NASA Formal Methods (NFM) 2016
  11. A Term Rewriting Approach to Analyze High Level Petri Nets Xudong He, Reng Zeng, Su Liu, Zhuo Sun, Kyungmin Bae International Symposium on Theoretical Aspects of Software Engineering (TASE) 2016
  12. Predicate Abstraction of Rewrite Theories Kyungmin Bae and José Meseguer Joint International Conference on Rewriting and Typed Lambda Calculi (RTA-TLCA) 2014
  13. Definition, Semantics, and Analysis of Multirate Synchronous AADL Kyungmin Bae, Peter Olveczky, and José Meseguer International Symposium on Formal Methods (FM) 2014
  14. Abstract Logical Model Checking of Infinite-State Systems Using Narrowing Kyungmin Bae, Santiago Escobar and José Meseguer International Conference on Rewriting Techniques and Applications (RTA) 2013
  15. The SynchAADL2Maude Tool Kyungmin Bae, Peter Olveczky, José Meseguer, and Abdullah Al-Nayeem International Conference on Fundamental Approaches to Software Engineering (FASE) 2012
  16. Formal Patterns for Multi-Rate Distributed Real-Time Systems Kyungmin Bae, José Meseguer, and Peter Olveczky International Symposium on Formal Aspects of Component Software (FACS) 2012
  17. State/Event-based LTL Model Checking under Parametric Generalized Fairness Kyungmin Bae and José Meseguer International Conference on Computer Aided Verification (CAV) 2011
  18. Synchronous AADL and its Formal Analysis in Real-Time Maude Kyungmin Bae, Peter Olveczky, Abdullah Al-Nayeem and José Meseguer International Conference on Formal Engineering Methods (ICFEM) 2011
  19. 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) 2009

Journal Articles

  1. Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL Jaehun Lee, Kyungmin Bae, Peter Olveczky, Sharon Kim, and Minseok Kang Software Tools for Technology Transfer 24: 911–948 2022
  2. Symbolic State Space Reduction with Guarded Terms for Rewriting Modulo SMT Kyungmin Bae and Camilo Rocha Science of Computer Programming 178: 20-42 2019
  3. Designing and Verifying Distributed Cyber-Physical Systems using Multirate PALS: An Airplane Turning Control System Case Study Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Olveczky Science of Computer Programming 103:13-50 2015
  4. Model Checking Linear Temporal Logic of Rewriting Formulas under Localized Fairness Kyungmin Bae, and José Meseguer Science of Computer Programming 99 2015
  5. Formal Patterns for Multirate Distributed Real-Time Systems (extended version) Kyungmin Bae, José Meseguer, and Peter Olveczky Science of Computer Programming 91, Part A 2014
  6. 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 Papers

  1. Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Ölveczky, Laure Petrucci, Fredrik Rømming ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS) 2022
  2. Symbolic Reachability Analysis of Distributed Systems using Narrowing and Heuristic Search Byeongjee Kang, Kyungmin Bae ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS) 2022
  3. Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT Jaeseo Lee, Sangki Kim, Kyungmin Bae ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS) 2022
  4. Maude-SE: a Tight Integration of Maude and SMT Solvers Geunyeol Yu and Kyungmin Bae International Workshop on Rewriting Logic and its Applications (WRLA) 2020
  5. An Architecture for Hybrid Planning and Execution Robert P. Goldman, Dan Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae AAAI-16 Workshop on Planning for Hybrid Systems 2016
  6. SMT Encoding of Hybrid Systems in dReal Kyungmin Bae, Soonho Kong, and Sicun Gao International Workshop on Applied veRification for Continuous and Hybrid Systems 2015
  7. Hybrid Multirate PALS Kyungmin Bae and Peter C. Olveczky Logic, Rewriting, and Concurrency 2015
  8. Infinite-State Model Checking of LTLR Formulas Unsing Narrowing Kyungmin Bae and José Meseguer International Workshop on Rewriting Logic and its Applications (WRLA) 2014
  9. PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Olveczky International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS) 2012
  10. Model Checking LTLR Formulas under Localized Fairness Kyungmin Bae and José Meseguer International Workshop on Rewriting Logic and its Applications (WRLA) 2012
  11. Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models Kyungmin Bae and Peter C. Olveczky International Workshop on Rewriting Techniques for Real-Time Systems 2010
  12. The Linear Temporal Logic of Rewriting Maude Model Checker Kyungmin Bae and José Meseguer International Workshop on Rewriting Logic and its Applications (WRLA) 2010
  13. A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting Kyungmin Bae and José Meseguer International Workshop on Rule-Based Programming 2008

Books

  • Rewriting Logic and Its Applications - 14th International Workshop, WRLA@ETAPS 2022, Munich, Germany, April 2-3, 2022, Revised Selected Papers Kyungmin Bae Lecture Notes in Computer Science 13252, Springer 2022
  • FormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering, Seoul, Republic of Korea, July 13, 2020 Kyungmin Bae, Domenico Bianculli, Stefania Gnesi, and Nico Plat ACM 2020
  • Formal Aspects of Component Software - 15th International Conference, FACS 2018, Pohang, South Korea, October 10-12, 2018, Proceedings Kyungmin Bae and Peter Olveczky Lecture Notes in Computer Science 11222, Springer 2018
  • Rewriting-based model checking methods Kyungmin Bae, PhD Dissertation, Department of Computer Science, University of Illinois at Urbana-Champaign, USA 2014 (link)

Education

Employment

Honors and Awards