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 219
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. Formal Analysis of Networked PLC Controllers Interacting with Physical Environments Jaeseo Lee and Kyungmin Bae Static Analysis Symposia (SAS) 2025 (to appear)
  2. Rigorous Model Engineering of Hierarchical Multirate CPSs in MR-HybridSynchAADL Jaehun Lee, Kyungmin Bae and Peter Olveczky International Symposium on Leveraging Applications of Formal Methods (ISoLA) 2024
  3. Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption Jaeseo Lee and Kyungmin Bae International Symposium on Formal Methods (FM) 2024
  4. Formal Specification of Trusted Execution Environment APIs Geunyeol Yu, Seunghyun Chae, Kyungmin Bae, and Sungkun Moon International Conference on Fundamental Approaches to Software Engineering (FASE) 2024
  5. Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Ölveczky, Laure Petrucci, and Fredrik Romming International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets) 2023
  6. Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL Kyungmin Bae and Peter Olveczky International Conference on Formal Aspects of Component Software (FACS) 2023
  7. 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
  8. 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
  9. 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
  10. 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
  11. 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
  12. 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
  13. Modular SMT-Based Analysis of Nonlinear Hybrid Systems Kyungmin Bae and Sicun Gao International Conference on Formal Methods in Computer-Aided Design (FMCAD) 2017
  14. Guarded Terms for Rewriting modulo SMT Kyungmin Bae and Camilo Rocha International Conference on Formal Aspects of Component Software (FACS) 2017
  15. 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
  16. 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
  17. 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
  18. Predicate Abstraction of Rewrite Theories Kyungmin Bae and José Meseguer Joint International Conference on Rewriting and Typed Lambda Calculi (RTA-TLCA) 2014
  19. Definition, Semantics, and Analysis of Multirate Synchronous AADL Kyungmin Bae, Peter Olveczky, and José Meseguer International Symposium on Formal Methods (FM) 2014
  20. 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
  21. The SynchAADL2Maude Tool Kyungmin Bae, Peter Olveczky, José Meseguer, and Abdullah Al-Nayeem International Conference on Fundamental Approaches to Software Engineering (FASE) 2012
  22. 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
  23. State/Event-based LTL Model Checking under Parametric Generalized Fairness Kyungmin Bae and José Meseguer International Conference on Computer Aided Verification (CAV) 2011
  24. 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
  25. 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. SMT-based robust model checking for signal temporal logic Jia Lee, Geunyeol Yu, and Kyungmin Bae Science of Computer Programming 246: 103332 2025
  2. Narrowing and heuristic search for symbolic reachability analysis of concurrent object-oriented systems Byeongjee Kang and Kyungmin Bae Science of Computer Programming 235: 103097 2024
  3. A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Ölveczky, Laure Petrucci, and Fredrik Romming Fundamenta Informaticae 192, Issue 3-4 2024
  4. Symbolic analysis and parameter synthesis for networks of parametric timed automata with global variables using Maude and SMT solving Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Olveczky, Laure Petrucci, and Fredrik Romming Science of Computer Programming 233: 103074 2024
  5. 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
  6. Symbolic State Space Reduction with Guarded Terms for Rewriting Modulo SMT Kyungmin Bae and Camilo Rocha Science of Computer Programming 178: 20-42 2019
  7. 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
  8. Model Checking Linear Temporal Logic of Rewriting Formulas under Localized Fairness Kyungmin Bae, and José Meseguer Science of Computer Programming 99 2015
  9. 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
  10. 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. Semantics and formal analysis of Lingua Franca CPS specifications in rewriting logic Mircea Marin, Peter Olveczky, Mario Reja, Mikheil Rukhaia, and Kyungmin Bae Marjan Festschrift at FSEN 2025
  2. A Flexible Framework for Integrating Maude and SMT Solvers Using Python Geunyeol Yu and Kyungmin Bae International Workshop on Rewriting Logic and its Applications (WRLA) 2024
  3. Verifying Invariants by Deductive Model Checking‹ Kyungmin Bae, Santiago Escobar, Raúl López-Rueda, José Meseguer, and Julia Sapiña International Workshop on Rewriting Logic and its Applications (WRLA) 2024
  4. Formal Model Engineering of Synchronous CPS Designs in AADL Kyungmin Bae and Peter Olveczky 2nd ADEPT workshop: AADL by its practitioners (ADEPT) 2023
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. Hybrid Multirate PALS Kyungmin Bae and Peter C. Olveczky Logic, Rewriting, and Concurrency 2015
  12. Infinite-State Model Checking of LTLR Formulas Unsing Narrowing Kyungmin Bae and José Meseguer International Workshop on Rewriting Logic and its Applications (WRLA) 2014
  13. 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
  14. Model Checking LTLR Formulas under Localized Fairness Kyungmin Bae and José Meseguer International Workshop on Rewriting Logic and its Applications (WRLA) 2012
  15. 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
  16. The Linear Temporal Logic of Rewriting Maude Model Checker Kyungmin Bae and José Meseguer International Workshop on Rewriting Logic and its Applications (WRLA) 2010
  17. 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