POSTECH SV Lab - Publications

Efficient Verification of Lingua Franca Programs
Peter Olveczky, Mario Reja, Mikheil Rukhaia, Kyungmin Bae, and Mircea Marin
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (to appear), 2026

모델체킹을 위한 강화학습 기반 휴리스틱 학습
강혜윤, 손병호, 배경민
한국소프트웨어공학학술대회 논문집, 2026

A Formal Executable Semantics of PROMELA
Byoungho Son and Kyungmin Bae
International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2026

MR-HybridSynchAADL: formal modeling and analysis of multirate CPSs with advanced control programs and continuous dynamics
Jaehun Lee, Kyungmin Bae, and Peter Ölveczky
Software Tools for Technology Transfer (STTT), 2025

DM-Check: Verifying invariants of concurrent systems by deductive model checking
Kyungmin Bae, Santiago Escobar, Raúl López-Rueda, José Meseguer, and Julia Sapiña
Journal of Logical and Algebraic Methods in Programming 149, 2025

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

Modeling and Analyzing Real-Time Systems in Rewriting Logic
Kyungmin Bae, Carlos Olarte, and Peter Ölveczky
Gul Agha Festschrift Symposium, 2025

SMT-based robust model checking for signal temporal logic
Jia Lee, Geunyeol Yu, and Kyungmin Bae
Science of Computer Programming, 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

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

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

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

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

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

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

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

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

Formal Model Engineering of Synchronous CPS Designs in AADL
Kyungmin Bae and Peter Olveczky
2nd ADEPT workshop: AADL by its practitioners (ADEPT), 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

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

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

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

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

Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Ölveczky, Laure Petrucci, and Fredrik Rømming
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 Olveczky
International Symposium On Leveraging Applications of Formal Methods (ISOLA), 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

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

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

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

Maude-SE: a Tight Integration of Maude and SMT Solvers
Geunyeol Yu and Kyungmin Bae
International Workshop on Rewriting Logic and its Applications, 2020

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

구조적 성질을 활용한 심층신경망의 정형검증 기법
정문현, 배경민
한국정보과학회 학술발표논문집, 2020

심층신경망의 정형검증 기법 소개
배경민
정보과학회지, 2020

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

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

Symbolic State Space Reduction with Guarded Terms for Rewriting Modulo SMT
Kyungmin Bae and Camilo Rocha
Science of Computer Programming 178: 20-42, 2019

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

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

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

Modular SMT-Based Analysis of Nonlinear Hybrid Systems
Kyungmin Bae and Sicun Gao
International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2017

Guarded Terms for Rewriting modulo SMT
Kyungmin Bae and Camilo Rocha
International Conference on Formal Aspects of Component Software (FACS), 2017

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

A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control
Robert P. Goldman, Daniel Bryce, Michael J. S. Pelican, David J. Musliner, and Kyungmin Bae
International Symposium on NASA Formal Methods (NFM), 2016

A Term Rewriting Approach to Analyze High Level Petri Nets
Xudong He, Reng Zeng, Su Liu, Zhuo Sun, and Kyungmin Bae
International Symposium on Theoretical Aspects of Software Engineering (TASE), 2016

An Architecture for Hybrid Planning and Execution
Robert P. Goldman, Dan Bryce, Michael J. S. Pelican, David J. Musliner, and Kyungmin Bae
AAAI-16 Workshop on Planning for Hybrid Systems, 2016

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

Model Checking Linear Temporal Logic of Rewriting Formulas under Localized Fairness
Kyungmin Bae, and José Meseguer
Science of Computer Programming 99, 2015

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

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

Predicate Abstraction of Rewrite Theories
Kyungmin Bae and José Meseguer
Joint International Conference on Rewriting and Typed Lambda Calculi (RTA-TLCA), 2014

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

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

Infinite-State Model Checking of LTLR Formulas Unsing Narrowing
Kyungmin Bae and José Meseguer
International Workshop on Rewriting Logic and its Applications, 2014

Rewriting-based model checking methods
Kyungmin Bae
PhD Dissertation, Department of Computer Science, University of Illinois at Urbana-Champaign, USA, 2014

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

The SynchAADL2Maude Tool
Kyungmin Bae, Peter Olveczky, José Meseguer, and Abdullah Al-Nayeem
International Conference on Fundamental Approaches to Software Engineering (FASE), 2012

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

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

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

Model Checking LTLR Formulas under Localized Fairness
Kyungmin Bae and José Meseguer
International Workshop on Rewriting Logic and its Applications, 2012

State/Event-based LTL Model Checking under Parametric Generalized Fairness
Kyungmin Bae and José Meseguer
International Conference on Computer Aided Verification (CAV), 2011

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

Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models
Kyungmin Bae and Peter C. Olveczky
nternational Workshop on Rewriting Techniques for Real-Time Systems, 2010

The Linear Temporal Logic of Rewriting Maude Model Checker
Kyungmin Bae and José Meseguer
International Workshop on Rewriting Logic and its Applications, 2010

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

A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting
Kyungmin Bae and José Meseguer
International Workshop on Rule-Based Programming, 2008