Publications

2025

Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
Jaeseo Lee and Kyungmin Bae
Static Analysis Symposium (SAS), 2025

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

SMT-based robust model checking for signal temporal logic
Jia Lee, Geunyeol Yu, and Kyungmin Bae
Science of Computer Programming, 2025

Model Checking of Signal Temporal Logic
Jia Lee
Ph.D Dissertation, Department of Computer Science, POSTECH, 2025

2024

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

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

A Flexible Framework for Integrating Maude and SMT Solvers Using Python
Geunyeol Yu and Kyungmin Bae
SInternational Workshop on Rewriting Logic and its Applications (WRLA), 2024

Narrowing and Heuristic Search for Symbolic Reachability Analysis of Concurrent Object-Oriented Systems
Byeongjee Kang and Kyungmin Bae
Science of Computer Programming, 2024

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, 2024

Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption
Jaeseo Lee and Kyungmin Bae
International Symposium on Formal Methods (FM), 2024

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

2023

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

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

Formal Model Engineering of Synchronous CPS Designs in AADL
Kyungmin Bae and Peter Olveczky
2nd ADEPT Workshop: AADL by its Practitioners (ADEPT), 2023

2022

Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT
Jaeseo Lee, Sangki Kim, and Kyungmin Bae
Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), 2022

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

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

Symbolic Reachability Analysis of Distributed Systems Using Narrowing and Heuristic Search
Byeongjee Kang and Kyungmin Bae
ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), 2022

Bounded Model Checking of PLC ST Programs Using Rewriting Modulo SMT
Jaeseo Lee, Sangki Kim, and Kyungmin Bae
ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), 2022

심층 신경망의 효과적인 정형 검증을 위한 계층별 요약 기법
연주은, 채승현, 배경민
정보과학회논문지, 2022

An Extension of HybridSynchAADL and Its Application to Collaborating Autonomous UAVs
Jaehun Lee, Kyungmin Bae, and Peter Csaba Ölveczky
International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA), 2022

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 (STTT), 2022

Formal Specification and Analysis of PLC and OSEK/VDX OS using Maude
Sangki Kim
MS Dissertation, Department of Computer Science, POSTECH, 2022

Abstractions for Verifying DNN
Jueun Yeon
MS Dissertation, Department of Computer Science, POSTECH, 2022

Extending the HybridSynchAADL Modeling Language and Tool
Jaehun Lee
MS Dissertation, Department of Computer Science, POSTECH, 2022

2021

계층별 요약을 이용한 심층 신경망 정형 검증 기법
연주은, 채승현, 배경민
한국정보과학회 학술발표논문집, 2021

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

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

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

구조적 성질을 활용한 심층신경망의 SMT 기반 정형검증 기법
정문현, 배경민
정보과학회논문지, 2021

Formal Verification of Deep Neural Networks using Structural Properties
Moonhyeon Chung
MS Dissertation, Department of Computer Science, POSTECH, 2021

2020

<a href="{"display"=>nil}">Maude-SE: a Tight Integration of Maude and SMT Solvers</a>
Geunyeol Yu and Kyungmin Bae
International Workshop on Rewriting Logic and its Applications, 2020

<a href="{"display"=>nil}">구조적 성질을 활용한 심층신경망의 정형검증 기법</a>
정문현, 배경민
한국정보과학회 학술발표논문집, 2020

<a href="{"display"=>nil}">심층신경망의 정형검증 기법 소개</a>
배경민
정보과학회지, 2020

HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous Cyber-Physical Systems in AADL
Sharon Kim
MS Dissertation, Department of Computer Science, POSTECH, 2020

2019

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

<a href="{"display"=>nil}">Symbolic State Space Reduction with Guarded Terms for Rewriting Modulo SMT</a>
Kyungmin Bae and Camilo Rocha
Science of Computer Programming 178: 20-42, 2019

CPI 보안 강화 코드 변환의 실용적인 동등성 검사 기법
이재서, 최태형, 이규호, 유재관, 배경민
정보과학회논문지, 2019

Maude를 통한 분산 드론 시스템의 정형 분석
김사론, 배경민
한국정보과학회 학술발표논문집, 2019

2018

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

2017

<a href="{"display"=>nil}">Modular SMT-Based Analysis of Nonlinear Hybrid Systems</a>
Kyungmin Bae and Sicun Gao
International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2017

<a href="{"display"=>nil}">Guarded Terms for Rewriting modulo SMT</a>
Kyungmin Bae and Camilo Rocha
International Conference on Formal Aspects of Component Software (FACS), 2017

2016

<a href="{"display"=>nil}">SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems</a>
Kyungmin Bae, Peter Olveczky, Soonho Kong, Sicun Gao, and Edmund M. Clarke
ACM International Conference on Hybrid Systems: Computation and Control (HSCC), 2016

<a href="{"display"=>nil}">A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control</a>
Robert P. Goldman, Daniel Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae
International Symposium on NASA Formal Methods (NFM), 2016

<a href="{"display"=>nil}">A Term Rewriting Approach to Analyze High Level Petri Nets</a>
Xudong He, Reng Zeng, Su Liu, Zhuo Sun, Kyungmin Bae
International Symposium on Theoretical Aspects of Software Engineering (TASE), 2016

<a href="{"display"=>nil}">An Architecture for Hybrid Planning and Execution</a>
Robert P. Goldman, Dan Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae
AAAI-16 Workshop on Planning for Hybrid Systems, 2016

2015

Hybrid Multirate PALS
Kyungmin Bae and Peter C. Olveczky
Logic, Rewriting, and Concurrency, 2015

<a href="{"display"=>nil}">Designing and Verifying Distributed Cyber-Physical Systems using Multirate PALS: An Airplane Turning Control System Case Study</a>
Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Olveczky
Science of Computer Programming 103:13-50, 2015

<a href="{"display"=>nil}">Model Checking Linear Temporal Logic of Rewriting Formulas under Localized Fairness</a>
Kyungmin Bae, and José Meseguer
Science of Computer Programming 99, 2015

<a href="{"display"=>nil}">SMT Encoding of Hybrid Systems in dReal</a>
Kyungmin Bae, Soonho Kong, and Sicun Gao
International Workshop on Applied veRification for Continuous and Hybrid Systems, 2015

2014

<a href="{"display"=>nil}">Predicate Abstraction of Rewrite Theories</a>
Kyungmin Bae and José Meseguer
Joint International Conference on Rewriting and Typed Lambda Calculi (RTA-TLCA), 2014

<a href="{"display"=>nil}">Definition, Semantics, and Analysis of Multirate Synchronous AADL</a>
Kyungmin Bae, Peter Olveczky, and José Meseguer
International Symposium on Formal Methods (FM), 2014

<a href="{"display"=>nil}">Formal Patterns for Multirate Distributed Real-Time Systems (extended version)</a>
Kyungmin Bae, José Meseguer, and Peter Olveczky
Science of Computer Programming 91, Part A, 2014

<a href="{"display"=>nil}">Infinite-State Model Checking of LTLR Formulas Unsing Narrowing</a>
Kyungmin Bae and José Meseguer
International Workshop on Rewriting Logic and its Applications, 2014

<a href="{"display"=>nil}">Rewriting-based model checking methods</a>
Kyungmin Bae
PhD Dissertation, Department of Computer Science, University of Illinois at Urbana-Champaign, USA, 2014

2013

<a href="{"display"=>nil}">Abstract Logical Model Checking of Infinite-State Systems Using Narrowing</a>
Kyungmin Bae, Santiago Escobar and José Meseguer
International Conference on Rewriting Techniques and Applications (RTA), 2013

2012

<a href="{"display"=>nil}">The SynchAADL2Maude Tool</a>
Kyungmin Bae, Peter Olveczky, José Meseguer, and Abdullah Al-Nayeem
International Conference on Fundamental Approaches to Software Engineering (FASE), 2012

<a href="{"display"=>nil}">Formal Patterns for Multi-Rate Distributed Real-Time Systems</a>
Kyungmin Bae, José Meseguer, and Peter Olveczky
International Symposium on Formal Aspects of Component Software (FACS), 2012

<a href="{"display"=>nil}">Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude</a>
Kyungmin Bae, Peter C. Olveczky, Thomas H. Feng, Edward A. Lee and Stavros Tripakis
Science of Computer Programming 77(12), 2012

<a href="{"display"=>nil}">PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude</a>
Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Olveczky
International Workshop on Formal Techniques for Safety-Critical Systems, 2012

<a href="{"display"=>nil}">Model Checking LTLR Formulas under Localized Fairness</a>
Kyungmin Bae and José Meseguer
International Workshop on Rewriting Logic and its Applications, 2012

2011

<a href="{"display"=>nil}">State/Event-based LTL Model Checking under Parametric Generalized Fairness</a>
Kyungmin Bae and José Meseguer
International Conference on Computer Aided Verification (CAV), 2011

<a href="{"display"=>nil}">Synchronous AADL and its Formal Analysis in Real-Time Maude</a>
Kyungmin Bae, Peter Olveczky, Abdullah Al-Nayeem and José Meseguer
International Conference on Formal Engineering Methods (ICFEM), 2011

2010

<a href="{"display"=>nil}">Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models</a>
Kyungmin Bae and Peter C. Olveczky
nternational Workshop on Rewriting Techniques for Real-Time Systems, 2010

<a href="{"display"=>nil}">The Linear Temporal Logic of Rewriting Maude Model Checker</a>
Kyungmin Bae and José Meseguer
International Workshop on Rewriting Logic and its Applications, 2010

2009

<a href="{"display"=>nil}">Verifying Ptolemy II Discrete-Event Models using Real-Time Maude</a>
Kyungmin Bae, Peter C. Olveczky, Thomas H. Feng and Stavros Tripakis
International Conference on Formal Engineering Methods (ICFEM), 2009

2008

<a href="{"display"=>nil}">A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting</a>
Kyungmin Bae and José Meseguer
International Workshop on Rule-Based Programming, 2008