교원검색

Profile

Profile.
Name	Kyungmin Bae
Organization	Dept of Computer Science & Enginrg
Telephone	054-279-2256
E-mail	kmbae@postech.ac.kr
Homepage

Education

2007.08 ~ 2014.08 UNIV. OF ILLINOIS AT URBANA CHAMPAIGN (통합-Computer Scinece)
2000.03 ~ 2004.02 한국과학기술원 (학사-전산학 (수학 복수전공))

Career

2015.07 ~ 2016.01 : SRI INTERNATIONAL COMPUTER SCIENCE LABORATORY
2014.10 ~ 2015.07 : CARNEGIE MELLON UNIV. DEPT. OF COMPUTER SCIENCE

Profession

Formal methods
Formal verification
Software engineering

International

Symbolic state space reduction with guarded terms for rewriting modulo SMT, SCIENCE OF COMPUTER PROGRAMMING, , 178, 20-42 (2019)
Formal Aspects of Component Software - 15th International Conference, FACS 2018, Pohang, South Korea, October 10-12, 2018, Proceedings., Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), , 11222, VI- (2018)
Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study, SCIENCE OF COMPUTER PROGRAMMING, , 103, 13-50 (2015)
Model checking linear temporal logic of rewriting formulas under localized fairness, SCIENCE OF COMPUTER PROGRAMMING, , 99, 193-234 (2015)
Hybrid Multirate PALS, LOGIC, REWRITING, AND CONCURRENCY, , 9200, 114-134 (2015)
Formal patterns for multirate distributed real-time systems, SCIENCE OF COMPUTER PROGRAMMING, , 91, 3-44 (2014)
Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude, SCIENCE OF COMPUTER PROGRAMMING, , 77, 1235-1271 (2012)
A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting, Electronic Notes in Theoretical Computer Science, , 290, 19-36 (2012)

Domestic Journal Papers

Lightweight Equivalence Checking of Code Transformation for Code Pointer Integrity, 정보과학회논문지, , 46, 1279-1290 (2019)

General Journal Papers

Conference Proceedings

Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation, Proc. ACM Program. Lang. 3, 0, 0, - (2019)
Guarded Terms for Rewriting Modulo SMT , FACS 2017: Formal Aspects of Component Software, 0, 0, 78-97 (2017)
Modular SMT-based analysis of nonlinear hybrid systems , Formal Methods in Computer Aided Design (FMCAD), 2017, 0, 0, 180-187 (2017)
A Term Rewriting Approach to Analyze High Level Petri Nets, TASE 2016, 0, 0, - (2016)
A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control, NASA FORMAL METHODS, 0, 0, - (2016)
SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems, PROCEEDINGS OF HSCC16, 0, 0, - (2016)
An Architecture for Hybrid Planning and Execution, The Workshops of the Thirtieth AAAI Conference on Artificial Intelligence: Technical Reports WS-16-01 – WS-16-15, 0, 0, - (2016)
SMT Encoding of Hybrid Systems in dReal, EPIC SERIES IN COMPUTING, 0, 0, - (2015)
Predicate Abstraction of Rewrite Theories, REWRITING AND TYPED LAMBDA CALCULI, 0, 0, - (2014)
Definition, Semantics, and Analysis of Multirate Synchronous AADL, FM 2014: FORMAL METHODS, 0, 0, - (2014)
Infinite-State Model Checking of LTLR Formulas Using Narrowing, REWRITING LOGIC AND ITS APPLICATIONS, 0, 0, - (2014)
Abstract Logical Model Checking of Infinite-State Systems Using Narrowing, REWRITING TECHNIQUES AND APPLICATIONS, 0, 0, - (2013)
PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude, PROCEEDINGS FTSCS 2012, 0, 0, 5-21 (2012)
Formal Patterns for Multi-rate Distributed Real-Time Systems, FORMAL ASPECTS OF COMPONENT SOFTWARE, 0, 0, - (2012)
The SynchAADL2Maude Tool, FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 0, 0, - (2012)
Model Checking LTLR Formulas under Localized Fairness, REWRITING LOGIC AND ITS APPLICATIONS, 0, 0, 29-47 (2012)
Synchronous AADL and its Formal Analysis in Real-Time Maude., FORMAL METHODS AND SOFTWARE ENGINEERING, 0, 0, - (2011)
State/Event-Based LTL Model Checking under Parametric Generalized Fairness, COMPUTER AIDED VERIFICATION, 0, 0, - (2011)

Invited Talk or Presentations

Books

Composing Model-Based Analysis Tools, Springer, 307, Talcott, C(책임); Ananieva, S(공동); 배경민(공동); Combemale, B(공동); Heinrich, R(공동); Hills, M(공동); Khakpour, N(공동); Reussner, R(공동); Rumpe, B(공동); Scandurra, P(공동); Vangheluwe, H(공동) (2021)

Research Activities

배경민_신규부임교수 기자재지원(1차_학과), 포항공과대학교 (2016-2017)
배경민_신규부임교수 기자재지원(1차_대학), 포항공과대학교 (2016-2017)
배경민_신규부임교수 연구비지원(1차_학과), 포항공과대학교 (2016-2017)
배경민_신규부임교수 연구비지원(1차_대학), 포항공과대학교 (2016-2017)
MODELING AND VERIFICATION OF AUTONOMOUS CYBER-PHYSICAL AGENTS, 재단법인한국연구재단 (2016-2017)
배경민_신규부임교수 기자재지원(2차_대학), 포항공과대학교 (2017-2018)
배경민_신규부임교수 연구비지원(2차_대학), 포항공과대학교 (2017-2018)
배경민_신규부임교수 연구비지원(2차_학과), 포항공과대학교 (2017-2018)
보안강화코드 자동 변환 기술 분석 및 동등성 검증 기법 개발, 지티원 주식회사 (2017-2018)
인공지능 소프트웨어의 검증을 위한 알고리즘 연구, 포항공과대학교 (2017-2018)
배경민_신규부임교수 기자재지원(2차_학과), 포항공과대학교 (2017-2018)
학생인건비통합관리과제, 포항공대산학협력단 (2017-2040)
MODELING AND VERIFICATION OF AUTONOMOUS CYBER-PHYSICAL AGENTS, 재단법인한국연구재단 (2017-2018)
4.14172 이월과제, 재단법인한국연구재단 (2017-2018)
배경민_신규부임교수 연구비지원(3차_학과), 포항공과대학교 (2018-2019)
배경민_신규부임교수 연구비지원(3차_대학), 포항공과대학교 (2018-2019)
[CW]INTERNATIONAL CONFERENCE ON FORMAL ASPECTS OF COMPONENT SOFTWARE (FACS'18), 포항공과대학교 (2018-2019)
사이버물리시스템의 논리적 요구사항 검증 기법 연구, 포항공과대학교 (2018-2019)
MODELING AND VERIFICATION OF AUTONOMOUS CYBER-PHYSICAL AGENTS, 재단법인한국연구재단 (2018-2019)
4.15522/15725 이월과제, 재단법인한국연구재단 (2018-2019)
자체연구개발과제[2015년 신설], 포항공과대학교 (2018-2033)
MODEL CHECKING OF STL PROPERTIES FOR CPS SOFTWARE, 재단법인한국연구재단 (2019-2020)
MODELING AND VERIFICATION OF AUTONOMOUS CYBER-PHYSICAL AGENTS, 재단법인한국연구재단 (2019-2019)
4.17056/17168 이월과제, 재단법인한국연구재단 (2019-2019)
MODEL CHECKING OF STL PROPERTIES FOR CPS SOFTWARE, 재단법인한국연구재단 (2020-2021)
SAFETY VERIFICATION OF PLC SOFTWARE, 한국조선해양(주) (2020-2020)
4.17689 이월과제, 재단법인한국연구재단 (2020-2021)
MODEL CHECKING OF STL PROPERTIES FOR CPS SOFTWARE, 재단법인한국연구재단 (2021-2022)
4.0019436/4.0020160_이월과제, 재단법인한국연구재단 (2021-2022)
FORMAL MODELING AND VERIFICATION OF SECURE OS COMPONENTS, 삼성전자(주) (2022-2023)
DEVELOPMENT OF SECURITY VERIFICATION TECHNOLOGY AGAINST VULNERABILITIES TO ASSURE IOT/IIOT DEVICE SAFETY, 정보통신기획평가원 (2022-2022)
CODE-LEVEL AUTOMATED FORMAL VERIFICATION OF CPS SOFTWARE, 재단법인한국연구재단 (2022-2023)
DEVELOPMENT OF SECURITY VERIFICATION TECHNOLOGY AGAINST VULNERABILITIES TO ASSURE IOT, 정보통신기획평가원 (2023-2023)
4.0024268_이월과제, 정보통신기획평가원 (2023-2023)
ADVANCING MODEL-BASED DEVELOPMENT OF CPS SOFTWARE USING COMPLEXITY-REDUCING FORMAL PATTERNS, 재단법인한국연구재단 (2023-2024)