Publications

2026

conference Efficient Verification of Lingua Franca Programs
Peter Ölveczky, 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)
domestic 모델체킹을 위한 강화학습 기반 휴리스틱 학습
강혜윤, 손병호, 배경민
한국소프트웨어공학학술대회 논문집
conference A Formal Executable Semantics of PROMELA
Byoungho Son and Kyungmin Bae
International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)

2025

journal 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)
journal 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
journal SMT-based robust model checking for signal temporal logic
Jia Lee, Geunyeol Yu, and Kyungmin Bae
Science of Computer Programming
conference Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
Jaeseo Lee and Kyungmin Bae
Static Analysis Symposium (SAS)
conference Modeling and Analyzing Real-Time Systems in Rewriting Logic
Kyungmin Bae, Carlos Olarte, and Peter Ölveczky
Gul Agha Festschrift Symposium
domestic Maude를 활용한 웹 어셈블리 프로그램 모델 체킹
장혁순, 배경민
한국정보과학회 학술발표논문집
conference Semantics and formal analysis of Lingua Franca CPS specifications in rewriting logic
Mircea Marin, Peter Ölveczky, Mario Reja, Mikheil Rukhaia, and Kyungmin Bae
Marjan Festschrift at FSEN
thesis Model Checking of Signal Temporal Logic
Jia Lee
Doctoral Dissertation, Department of Computer Science and Engineering, POSTECH

2024

conference Rigorous Model Engineering of Hierarchical Multirate CPSs in MR-HybridSynchAADL
Jaehun Lee, Kyungmin Bae, and Peter Ölveczky
International Symposium on Leveraging Applications of Formal Methods (ISoLA)
journal 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
conference Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption
Jaeseo Lee and Kyungmin Bae
International Symposium on Formal Methods (FM)
journal Narrowing and Heuristic Search for Symbolic Reachability Analysis of Concurrent Object-Oriented Systems
Byeongjee Kang and Kyungmin Bae
Science of Computer Programming
domestic Formal Specification and Model Checking of TLS Software Security Requirements using Maude
이재훈, 배경민
Journal of KIISE Vol.51 No.5
domestic 신호시제논리 성질의 모델검증
배경민
정보과학회지 제42권 제5호(통권 제420호)
conference 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)
conference 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)
conference 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)
journal 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 Ölveczky, Laure Petrucci, and Fredrik Romming
Science of Computer Programming 233, 103074

2023

conference Formal Model Engineering of Synchronous CPS Designs in AADL
Kyungmin Bae and Peter Ölveczky
2nd ADEPT workshop: AADL by its practitioners (ADEPT)
conference Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL
Kyungmin Bae and Peter Ölveczky
International Conference on Formal Aspects of Component Software (FACS)
conference 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)

2022

journal Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL
Jaehun Lee, Kyungmin Bae, Peter Ölveczky, Sharon Kim, and Minseok Kang
Software Tools for Technology Transfer (STTT)
conference 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)
conference 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)
conference 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)
domestic 심층 신경망의 효과적인 정형 검증을 위한 계층별 요약 기법
연주은, 채승현, 배경민
Journal of KIISE Vol.49 No.11
conference An Extension of HybridSynchAADL and Its Application to Collaborating Autonomous UAVs
Jaehun Lee, Kyungmin Bae, and Peter Ölveczky
International Symposium On Leveraging Applications of Formal Methods (ISoLA)
thesis Formal Specification and Analysis of PLC and OSEK/VDX OS using Maude
Sangki Kim
Master's Thesis, Department of Computer Science and Engineering, POSTECH
thesis Abstractions for Verifying DNN
Jueun Yeon
Master's Thesis, Department of Computer Science and Engineering, POSTECH
conference STLmc: Robust STL Model Checking of Hybrid Systems using SMT
Geunyeol Yu, Jia Lee, and Kyungmin Bae
International Conference on Computer Aided Verification (CAV)
domestic Maude를 활용한 OSEK/VDX OS API 정형 명세 및 검증
김상기, 배경민
한국정보과학회 한국컴퓨터종합학술대회 논문집
book 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
thesis Extending the HybridSynchAADL Modeling Language and Tool
Jaehun Lee
Master's Thesis, Department of Computer Science and Engineering, POSTECH

2021

domestic 계층별 요약을 이용한 심층 신경망 정형 검증 기법
연주은, 채승현, 배경민
한국정보과학회 한국소프트웨어종합학술대회 논문집
conference 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)
conference MSYNC: A Generalized Formal Design Pattern for Virtually Synchronous Multirate Cyber-Physical Systems
Kyungmin Bae and Peter Ölveczky
International Conference on Embedded Software (EMSOFT)
conference HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL
Jaehun Lee, Sharon Kim, Kyungmin Bae, and Peter Ölveczky
International Conference on Computer Aided Verification (CAV)
domestic 구조적 성질을 활용한 심층신경망의 SMT 기반 정형검증 기법
정문현, 배경민
Journal of KIISE Vol.48 No.9
thesis Formal Verification of Deep Neural Networks using Structural Properties
Moonhyeon Chung
Master's Thesis, Department of Computer Science and Engineering, POSTECH

2020

conference Maude-SE: a Tight Integration of Maude and SMT Solvers
Geunyeol Yu and Kyungmin Bae
International Workshop on Rewriting Logic and its Applications (WRLA)
book 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
domestic 구조적 성질을 활용한 심층신경망의 정형검증 기법
정문현, 배경민
한국정보과학회 한국컴퓨터종합학술대회 논문집
domestic 심층신경망의 정형검증 기법 소개
배경민
정보과학회지 제38권 제4호(통권 제371호)
thesis HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous Cyber-Physical Systems in AADL
Sharon Kim
Master's Thesis, Department of Computer Science and Engineering, POSTECH

2019

conference 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)
journal Symbolic State Space Reduction with Guarded Terms for Rewriting Modulo SMT
Kyungmin Bae and Camilo Rocha
Science of Computer Programming 178: 20-42
domestic Maude를 통한 분산 드론 시스템의 정형 분석
김사론, 배경민
한국정보과학회 한국소프트웨어종합학술대회 논문집
domestic CPI 보안 강화 코드 변환의 실용적인 동등성 검사 기법
이재서, 최태형, 이규호, 유재관, 배경민
Journal of KIISE Vol.46 No.12

2018

book Formal Aspects of Component Software - 15th International Conference, FACS 2018, Pohang, South Korea, October 10-12, 2018, Proceedings
Kyungmin Bae and Peter Ölveczky
Lecture Notes in Computer Science 11222, Springer

2017

conference Modular SMT-Based Analysis of Nonlinear Hybrid Systems
Kyungmin Bae and Sicun Gao
International Conference on Formal Methods in Computer-Aided Design (FMCAD)
conference Guarded Terms for Rewriting modulo SMT
Kyungmin Bae and Camilo Rocha
International Conference on Formal Aspects of Component Software (FACS)

2016

conference 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)
conference 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)
conference SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems
Kyungmin Bae, Peter Ölveczky, Soonho Kong, Sicun Gao, and Edmund M. Clarke
ACM International Conference on Hybrid Systems: Computation and Control (HSCC)
conference 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

2015

conference SMT Encoding of Hybrid Systems in dReal
Kyungmin Bae, Soonho Kong, and Sicun Gao
International Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH)
conference Hybrid Multirate PALS
Kyungmin Bae and Peter C. Ölveczky
Logic, Rewriting, and Concurrency
journal 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 Ölveczky
Science of Computer Programming 103:13-50
journal Model Checking Linear Temporal Logic of Rewriting Formulas under Localized Fairness
Kyungmin Bae and José Meseguer
Science of Computer Programming 99

2014

journal Formal Patterns for Multirate Distributed Real-Time Systems (extended version)
Kyungmin Bae, José Meseguer, and Peter Ölveczky
Science of Computer Programming 91, Part A
conference Predicate Abstraction of Rewrite Theories
Kyungmin Bae and José Meseguer
Joint International Conference on Rewriting and Typed Lambda Calculi (RTA-TLCA)
conference Definition, Semantics, and Analysis of Multirate Synchronous AADL
Kyungmin Bae, Peter Ölveczky, and José Meseguer
International Symposium on Formal Methods (FM)
conference Infinite-State Model Checking of LTLR Formulas Unsing Narrowing
Kyungmin Bae and José Meseguer
International Workshop on Rewriting Logic and its Applications (WRLA)
thesis Rewriting-based model checking methods
Kyungmin Bae
Doctoral Dissertation, Department of Computer Science, University of Illinois at Urbana-Champaign

2013

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

2012

journal Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude
Kyungmin Bae, Peter C. Ölveczky, Thomas H. Feng, Edward A. Lee, and Stavros Tripakis
Science of Computer Programming 77(12)
conference Formal Patterns for Multi-Rate Distributed Real-Time Systems
Kyungmin Bae, José Meseguer, and Peter Ölveczky
International Symposium on Formal Aspects of Component Software (FACS)
conference The SynchAADL2Maude Tool
Kyungmin Bae, Peter Ölveczky, José Meseguer, and Abdullah Al-Nayeem
International Conference on Fundamental Approaches to Software Engineering (FASE)
conference Model Checking LTLR Formulas under Localized Fairness
Kyungmin Bae and José Meseguer
International Workshop on Rewriting Logic and its Applications (WRLA)
conference PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude
Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Ölveczky
International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)

2011

conference Synchronous AADL and its Formal Analysis in Real-Time Maude
Kyungmin Bae, Peter Ölveczky, Abdullah Al-Nayeem, and José Meseguer
International Conference on Formal Engineering Methods (ICFEM)
conference State/Event-based LTL Model Checking under Parametric Generalized Fairness
Kyungmin Bae and José Meseguer
International Conference on Computer Aided Verification (CAV)

2010

conference Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models
Kyungmin Bae and Peter C. Ölveczky
International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS)
conference The Linear Temporal Logic of Rewriting Maude Model Checker
Kyungmin Bae and José Meseguer
International Workshop on Rewriting Logic and its Applications (WRLA)

2009

conference Verifying Ptolemy II Discrete-Event Models using Real-Time Maude
Kyungmin Bae, Peter C. Ölveczky, Thomas H. Feng, and Stavros Tripakis
International Conference on Formal Engineering Methods (ICFEM)

2008

conference A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting
Kyungmin Bae and José Meseguer
International Workshop on Rule-Based Programming
No publications match your search.