POSTECH SV Lab - Publications

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

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

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

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

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

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

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

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

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

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, 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, 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, Kyungmin Bae
AAAI-16 Workshop on Planning for Hybrid Systems, 2016

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

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

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