교원프로필

배경민 사진
교원에 대한 정보를 나타내는 표입니다.
성명 배경민
소속 컴퓨터공학과
전화번호 054-279-2256
E-mail kmbae@postech.ac.kr

학력

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

주요경력

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

전문분야

  • Formal methods
  • Formal verification
  • Software engineering

학술지

국제전문학술지

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

국내전문학술지

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

일반학술지

학술회의논문

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

학회발표

단행본

  • Composing Model-Based Analysis Tools, Springer, 307, BAE, K (2021)

연구실적

  • 배경민_신규부임교수 기자재지원(1차_학과), 포항공과대학교 (2016-2017)
  • 배경민_신규부임교수 기자재지원(1차_대학), 포항공과대학교 (2016-2017)
  • 배경민_신규부임교수 연구비지원(1차_학과), 포항공과대학교 (2016-2017)
  • 배경민_신규부임교수 연구비지원(1차_대학), 포항공과대학교 (2016-2017)
  • 자율 사이버물리 에이전트를 위한 모델링 및 검증 기법 연구, 재단법인한국연구재단 (2016-2017)
  • 배경민_신규부임교수 기자재지원(2차_대학), 포항공과대학교 (2017-2018)
  • 배경민_신규부임교수 연구비지원(2차_대학), 포항공과대학교 (2017-2018)
  • 배경민_신규부임교수 연구비지원(2차_학과), 포항공과대학교 (2017-2018)
  • 보안강화코드 자동 변환 기술 분석 및 동등성 검증 기법 개발, 지티원 주식회사 (2017-2018)
  • 인공지능 소프트웨어의 검증을 위한 알고리즘 연구, 포항공과대학교 (2017-2018)
  • 배경민_신규부임교수 기자재지원(2차_학과), 포항공과대학교 (2017-2018)
  • 학생인건비통합관리과제, 포항공대산학협력단 (2017-2040)
  • 자율 사이버물리 에이전트를 위한 모델링 및 검증 기법 연구, 재단법인한국연구재단 (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)
  • 자율 사이버물리 에이전트를 위한 모델링 및 검증 기법 연구, 재단법인한국연구재단 (2018-2019)
  • 4.15522/15725 이월과제, 재단법인한국연구재단 (2018-2019)
  • 자체연구개발과제[2015년 신설], 포항공과대학교 (2018-2033)
  • CPS 소프트웨어의 논리적 요구사항 검증, 재단법인한국연구재단 (2019-2020)
  • 자율 사이버물리 에이전트를 위한 모델링 및 검증 기법 연구, 재단법인한국연구재단 (2019-2019)
  • 4.17056/17168 이월과제, 재단법인한국연구재단 (2019-2019)
  • CPS 소프트웨어의 논리적 요구사항 검증, 재단법인한국연구재단 (2020-2021)
  • 선박 통합제어시스템 소프트웨어의 신뢰성 검증 기술 개발, 한국조선해양(주) (2020-2020)
  • 4.17689 이월과제, 재단법인한국연구재단 (2020-2021)
  • CPS 소프트웨어의 논리적 요구사항 검증, 재단법인한국연구재단 (2021-2022)
  • 4.0019436/4.0020160_이월과제, 재단법인한국연구재단 (2021-2022)
  • SECURE OS에 대한 정형 명세 및 검증 기법 연구, 삼성전자(주) (2022-2023)
  • IOT/IIOT 디바이스 안전성 보장을 위한 취약점 보안검증 기술 개발, 정보통신기획평가원 (2022-2022)

IP

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