A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting. - Kyungmin Bae; José Meseguer 001 (RULE, 2008)

Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude. - Kyungmin Bae; Peter Csaba Ölveczky; Thomas Huining Feng; Stavros Tripakis (ICFEM, 2009)

The Linear Temporal Logic of Rewriting Maude Model Checker. - Kyungmin Bae; José Meseguer 001 (WRLA, 2010)

Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models - Kyungmin Bae; Peter Csaba Ölveczky (RTRTS, 2010)

State/Event-Based LTL Model Checking under Parametric Generalized Fairness. - Kyungmin Bae; José Meseguer 001 (CAV, 2011)

Synchronous AADL and Its Formal Analysis in Real-Time Maude. - Kyungmin Bae; Peter Csaba Ölveczky; Abdullah Al-Nayeem; José Meseguer 001 (ICFEM, 2011)

Formal Patterns for Multi-rate Distributed Real-Time Systems. - Kyungmin Bae; José Meseguer 001; Peter Csaba Ölveczky (FACS, 2012)

The SynchAADL2Maude Tool. - Kyungmin Bae; Peter Csaba Ölveczky; José Meseguer 001; Abdullah Al-Nayeem (FASE, 2012)

Model Checking LTLR Formulas under Localized Fairness. - Kyungmin Bae; José Meseguer 001 (WRLA, 2012)

PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude - Kyungmin Bae; Joshua Krisiloff; José Meseguer 001; Peter Csaba Ölveczky (FTSCS, 2012)

Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. - Kyungmin Bae; Peter Csaba Ölveczky; Thomas Huining Feng; Edward A. Lee; Stavros Tripakis (Sci. Comput. Program., 2012)

Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. - Kyungmin Bae; Santiago Escobar 001; José Meseguer 001 (RTA, 2013)

Definition, Semantics, and Analysis of Multirate Synchronous AADL. - Kyungmin Bae; Peter Csaba Ölveczky; José Meseguer 001 (FM, 2014)

Predicate Abstraction of Rewrite Theories. - Kyungmin Bae; José Meseguer 001 (RTA-TLCA, 2014)

Infinite-State Model Checking of LTLR Formulas Using Narrowing. - Kyungmin Bae; José Meseguer 001 (WRLA, 2014)

Formal patterns for multirate distributed real-time systems. - Kyungmin Bae; José Meseguer 001; Peter Csaba Ölveczky (Sci. Comput. Program., 2014)

Rewriting-based model checking methods - Kyungmin Bae (2014)

Hybrid Multirate PALS. - Kyungmin Bae; Peter Csaba Ölveczky (Logic, Rewriting, and Concurrency, 2015)

SMT Encoding of Hybrid Systems in dReal. - Kyungmin Bae; Soonho Kong; Sicun Gao (ARCH@CPSWeek, 2015)

Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study. - Kyungmin Bae; Joshua Krisiloff; José Meseguer 001; Peter Csaba Ölveczky (Sci. Comput. Program., 2015)

Model checking linear temporal logic of rewriting formulas under localized fairness. - Kyungmin Bae; José Meseguer 001 (Sci. Comput. Program., 2015)

An Architecture for Hybrid Planning and Execution. - Robert P. Goldman; Daniel Bryce; Michael J. S. Pelican; David J. Musliner; Kyungmin Bae (AAAI Workshop: Planning for Hybrid Systems, 2016)

SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems. - Kyungmin Bae; Peter Csaba Ölveczky; Soonho Kong; Sicun Gao; Edmund M. Clarke (HSCC, 2016)

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 (NFM, 2016)

A Term Rewriting Approach to Analyze High Level Petri Nets. - Xudong He; Reng Zeng; Su Liu; Zhuo Sun; Kyungmin Bae (TASE, 2016)

Guarded Terms for Rewriting Modulo SMT. - Kyungmin Bae; Camilo Rocha (FACS, 2017)

Modular SMT-based analysis of nonlinear hybrid systems. - Kyungmin Bae; Sicun Gao (FMCAD, 2017)

Bounded model checking of signal temporal logic properties using syntactic separation. - Kyungmin Bae; Jia Lee (Proc. ACM Program. Lang., 2019)

Symbolic state space reduction with guarded terms for rewriting modulo SMT. - Kyungmin Bae; Camilo Rocha (Sci. Comput. Program., 2019)

Formal aspects of component software (FACS 2018). - Kyungmin Bae; Peter Csaba Ölveczky (Sci. Comput. Program., 2020)

Foundations. - Carolyn L. Talcott; Sofia Ananieva; Kyungmin Bae; Benoît Combemale; Robert Heinrich; Mark Hills 001; Narges Khakpour; Ralf H. Reussner; Bernhard Rumpe; Patrizia Scandurra; Hans Vangheluwe; Francisco Durán 001; et al. (Composing Model-Based Analysis Tools, 2021)

Composition of Languages, Models, and Analyses. - Carolyn L. Talcott; Sofia Ananieva; Kyungmin Bae; Benoît Combemale; Robert Heinrich; Mark Hills 001; Narges Khakpour; Ralf H. Reussner; Bernhard Rumpe; Patrizia Scandurra; Hans Vangheluwe (Composing Model-Based Analysis Tools, 2021)

HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL. - Jaehun Lee; Sharon Kim; Kyungmin Bae; Peter Csaba Ölveczky (CAV (1), 2021)

Efficient SMT-Based Model Checking for Signal Temporal Logic. - Jia Lee; Geunyeol Yu; Kyungmin Bae (ASE, 2021)

MSYNC: A Generalized Formal Design Pattern for Virtually Synchronous Multirate Cyber-physical Systems. - Kyungmin Bae; Peter Csaba Ölveczky (ACM Trans. Embed. Comput. Syst., 2021)

STLmc: Robust STL Model Checking of Hybrid Systems Using SMT. - Geunyeol Yu; Jia Lee; Kyungmin Bae (CAV (1), 2022)

Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata. - Jaime Arias 001; Kyungmin Bae; Carlos Olarte; Peter Csaba Ölveczky; Laure Petrucci; Fredrik Rømming (FTSCS, 2022)

Symbolic Reachability Analysis of Distributed Systems using Narrowing and Heuristic Search. - Byeongjee Kang; Kyungmin Bae (FTSCS, 2022)

Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT. - Jaeseo Lee; Sangki Kim; Kyungmin Bae (FTSCS, 2022)

An Extension of HybridSynchAADL and Its Application to Collaborating Autonomous UAVs. - Jaehun Lee; Kyungmin Bae; Peter Csaba Ölveczky (ISoLA (3), 2022)

Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL. - Jaehun Lee; Kyungmin Bae; Peter Csaba Ölveczky; Sharon Kim; Minseok Kang (Int. J. Softw. Tools Technol. Transf., 2022)

Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving. - Jaime Arias 001; Kyungmin Bae; Carlos Olarte; Peter Csaba Ölveczky; Laure Petrucci; Fredrik Rømming (Petri Nets, 2023)

Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL. - Kyungmin Bae; Peter Csaba Ölveczky (FACS, 2023)

Bounded STL Model Checking for Hybrid Systems (Invited Talk). - Kyungmin Bae (FTSCS, 2023)

Formal Specification of Trusted Execution Environment APIs. - Geunyeol Yu; Seunghyun Chae; Kyungmin Bae; Sungkun Moon (FASE, 2024)

Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption. - Jaeseo Lee; Kyungmin Bae (FM (1), 2024)

Rigorous Model Engineering of Hierarchical Multirate CPSs in MR-HybridSynchAADL. - Jaehun Lee; Kyungmin Bae; Peter Csaba Ölveczky (ISoLA (2), 2024)

Verifying Invariants by Deductive Model Checking. - Kyungmin Bae; Santiago Escobar 001; Raúl López-Rueda; José Meseguer 001; Julia Sapiña (WRLA, 2024)

A Flexible Framework for Integrating Maude and SMT Solvers Using Python. - Geunyeol Yu; Kyungmin Bae (WRLA, 2024)

A Rewriting-logic-with-SMT-based Formal Analysis and Parameter Synthesis Framework for Parametric Time Petri Nets. - Jaime Arias 001; Kyungmin Bae; Carlos Olarte; Peter Csaba Ölveczky; Laure Petrucci (Fundam. Informaticae, 2024)

Symbolic analysis and parameter synthesis for networks of parametric timed automata with global variables using Maude and SMT solving. - Jaime Arias 001; Kyungmin Bae; Carlos Olarte; Peter Csaba Ölveczky; Laure Petrucci; Fredrik Rømming (Sci. Comput. Program., 2024)

Narrowing and heuristic search for symbolic reachability analysis of concurrent object-oriented systems. - Byeongjee Kang; Kyungmin Bae (Sci. Comput. Program., 2024)

Semantics and Formal Analysis of Lingua Franca CPS Specifications in Rewriting Logic. - Mircea Marin; Peter Csaba Ölveczky; Mario Reja; Mikheil Rukhaia; Kyungmin Bae (Rebeca for Actor Analysis in Action, 2025)

SMT-based robust model checking for signal temporal logic. - Jia Lee; Geunyeol Yu; Kyungmin Bae (Sci. Comput. Program., 2025)

Formal Analysis of Networked PLC Controllers Interacting with Physical Environments. - Jaeseo Lee; Kyungmin Bae (CoRR, 2025)