Profile

Kyungmin Bae 사진
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

Journal Papers

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)

IP

  • 배경민, 신호 시제 논리의 구문 분리 방법 및 장치, 한국, 10-2018-0050150 (2018)