2025
Ryeonggu Kwon and Gihwon Kwon, "CAMP: Counterexamples, Abstraction, MDPs, and Policy Refinement for Enhancing Safety, Stability, and Rewards in Reinforcement Learning", IEEE Access, Vol.13, pp.64750-64769, Apr. 2025
Daehui Jeong, Ryeonggu Kwon and Gihwon Kwon, "Probabilistic SIL Verification of a Synthesized Fault-tolerant Model for Reliable Safety Assessment", IEEE Access, Vol.13, Feb. 2025
Ryeonggu Kwon and Gihwon Kwon, "Optimization of State Clustering and Safety Verification in Deep Reinforcement Learning Using KMeans++ and Probabilistic Model Checking", IEEE Access, Vol.13, pp.28085-28097, Feb. 2025
Sohee Park and Gihwon Kwon, "Analyzing Key Features of Open Source Software Survivability with Random Forest", applied sciences, Vol.15, No.946, pp.1-19, Jan. 2025
Suhee Jo and Gihwon Kwon, "The Impact of Collaboration Patterns and Network Centrality on Long-Term Contribution in GitHub Project", applied sciences, Vol.15, No.352, pp.1-21, Jan. 2025
박승민, 권령구, 권기현, 이창율, "RAG 기반 LLM을 활용한 소프트웨어 프로젝트 성과 평가 및 지식 전수 시스템", 제27회 한국 소프트웨어공학학술대회(KCSE 2025) 논문집, Vol.27, No.1, 2025.01 [최우수논문상]
2024
Ryeonggu Kwon and Gihwon Kwon, "Safety Verification of Non-Deterministic Policies in Reinforcement Learning", IEEE Access, Vol.12, Dec. 2024
권령구, 권기현, 이창율, "연속 상태 공간에서 강화 학습 정책의 군집 기반 정형 검증 ", 2024년 한국정보기술학회 추계학술대회논문집, 2024.11 [우수논문상]
박승민, 조수희, 권령구, 권기현, 이창율 , "소프트웨어 프로젝트 성과 분석을 위한 LLM 기반 챗봇 개발", 2024년 한국정보기술학회 추계학술대회논문집, 2024.11
Sohee Park, Ryeonggu Kwon and Gihwon Kwon, "Survivability using Kaplan-Meier Survival Function and Polynomial Regression ", Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024), Poster presentation, Oct. 2024
Jiyoung Chang, Ryeonggu Kwon and Gihwon Kwon, "STPA-RL: Integrating Reinforcement Learning into STPA for Loss Scenario Exploration", applied sciences, Vol.14, No.2916, pp.1-19, Mar. 2024
Sohee Park, Ryeonggu Kwon and Gihwon Kwon, "Survivability Prediction of Open Source Software with Polynomial Regression", applied sciences, Vol.14, No.2812, pp.1-19, Mar. 2024
Suhee Jo, Ryeonggu Kwon and Gihwon Kwon, "Probabilistic Model Checking GitHub Repositories for Software Project Analysis", applied sciences, Vol.14, No.1260, pp.1-20, Feb. 2024
Ryeonggu Kwon, Gihwon Kwon, Sohee Park, Jiyoung Chang and Suhee Jo, "Applying Quantitative Model Checking to Analyze Safety in Reinforcement Learning", IEEE Access, Vol.12, pp.18957-18971, Feb. 2024
조수희, 장지영, 박소희, 권기현, "확률적 모델 체킹을 이용한 깃허브 기반의 프로젝트 참여자 기여 분석", 제26회 한국 소프트웨어공학학술대회 논문집, Vol.26, No.1, pp.10-11, 2024.01 [우수논문상]
2023
Jiyoung Chang, Ryeonggu Kwon and Gihwon Kwon, "Machine Learning-based STPA for Platform Screen Door", Proceedings of 10th ICAEIC-2023, Vol.6, No.1, pp.38-42, Feb. 2023 [Best Paper Award]
Sohee Park, Ryeonggu Kwon and Gihwon Kwon, "Prediction of Open-source Survivability with Supervised Machine Learning: A Case Study of KaKaoTalk", Proceedings of 10th ICAEIC-2023, Vol.6, No.1, pp.167-171, Feb. 2023
Suhee Jo and Gihwon Kwon, "Analysis of GitHub-based Software Development Project with Discrete-time Markov Chain", Proceedings of 10th ICAEIC-2023, Vol.6, No.1, pp.206-210, Feb. 2023
Ryeonggu Kwon and Gihwon Kwon, "Formal Verification of STPA with Model Checking", Scientific Journal of Gdynia Maritime University, No.125, pp.1-18, Mar. 2023
장지영, 권령구, 권기현, "STPA-RL: 강화학습을 이용한 STPA에서 손실 시나리오 분석", 한국정보기술학회 논문지, 27권 7호, pp.39-48, 2023.07
Ryeonggu Kwon and Gihwon Kwon, "Generating Controller of GR(1) Synthesis and Reinforcement Learning in Game-Solving", Journal of Korean Institute of Information Technology, Vol.27, No.7, pp.13-22, July 2023
박소희, 권령구, 권기현, "SMC를 이용한 액츄에이터의 불확실성에 따른 위험 평가", 한국정보기술학회 논문지, 27권 8호, pp.39-49, 2023.08
조수희, 권령구, 권기현, "강화 학습 모델의 안전성 평가 방법: 자율 주행 사례 연구", 한국정보기술학회 논문지, 27권 8호, pp.165-174, 2023.08
Faiza Sabir, Sarfaraz Ahmed and Gihwon Kwon, "Failure Analysis of Vital Sign Monitoring System in Digital Healthcare with FTA", Journal of Multimedia Information System, Vol.10, No.3, Sep. 2023
Ryeonggu Kwon and Gihwon Kwon, "Safety Constraint-Guided Reinforcement Learning with Linear Temporal Logic", Systems, Vol.11, No.11, pp.1~23, Nov. 2023
Jiyoung Chang, Ryeonggu Kwon and Gihwon Kwon, "Exploring Loss Scenarios of STPA with Reinforcement Learning: A Case Study of Platform Screen Door", Proceedings of the APSEC 2023, Dec. 2023
Suhee Jo, Ryeonggu Kwon and Gihwon Kwon, "Exploring Collaboration Patterns in GitHub using Discrete Time Markov Chain", Proceedings of the APSEC 2023, Dec. 2023
2022
김소연, 권기현, "AIAG-VDA 방법론 기반 SFMEA: 효과적인 자동차 SW 안전분석", 한국소프트웨어공학학술대회 논문집 (24권 1호), 2022.01 [우수논문상]
박소희, 권기현, 정대희, "고장 상태 시간의 불확실성이 신뢰ㆍ안정성에 미치는 영향 분석", 한국인터넷정보학회 2022 춘계학술발표대회 논문집 (23권 1호), 2022.04
김지훈, 권기현, 정대희, "IEC 61508 기반 2oo4 구조 SIL 검증 사례 연구", 한국인터넷정보학회 2022 춘계학술발표대회 논문집 (23권 1호), 2022.04
장지영, 권기현, 정대희, "SIL 검증을 위한 확률 모델 분석법 비교 연구", 한국인터넷정보학회 2022 춘계학술발표대회 논문집 (23권 1호), 2022.04
조수희, 권기현, 정대희, "IEC 61508 기반 KooN 아키텍처 설계에 따른 고장률 비교 분석", 한국인터넷정보학회 2022 춘계학술발표대회 논문집 (23권 1호), 2022.04
박소희, 권기현, 정대희, "대학생 SW 개발을 위한 경량화된 스크럼 프로세스", 한국정보기술학회 2022년도 하계종합학술대회 논문집 (17권 2호), 2022.06 [우수논문상(동상)]
장지영, 권기현, 정대희, 교육용 스크럼 프로세스 기반 도서관리시스템 개발 사례", 한국정보기술학회 2022년도 하계종합학술대회 논문집 (17권 1호), 2022.06 [우수논문상(동상)]
조수희, 권기현, 정대희, 스크럼 개발 프로세스를 지원하는 학생 친화적인 깃 플로우 모델", 한국정보기술학회 2022년도 하계종합학술대회 논문집 (17권 1호), 2022.06 [우수논문상(은상)]
Daehui Jeong, Gihwon Kwon, "Synthesizing Control Algorithm in GR(1) Specification for System Theoretic Hazard Analysis", Proceedings of the 17th Asia Pacific International Conference on Information Science and Technology(APIC-IST), Jun. 2022
Ngoc-Tung La, Gihwon Kwon, "Trapezoidal Uncertainty Estimation for Failure Rate Data in Safety Instrumented Systems", Advanced Engineering and ICT-Convergence Proceedings (Vol.5, No.2), Jul. 2002
Jiyoung Chang, Ngoc-Tung La, Gihwon Kwon, "SIL Verification of Safety Instrumented System with Variance Contribution Analysis", Advanced Engineering and ICT-Convergence Proceedings (Vol.5, No.2), Jul. 2002 [Best Paper Award]
Sohee Park, Ngoc-Tung La, Gihwon Kwon, "SIL Verification with Uncertain Down Time of Failure Advanced Engineering and ICT-Convergence Proceedings (Vol.5, No.2), Jul. 2002
Suhee Jo, Ngoc-Tung La, Gihwon Kwon, "Analysis of Students Term Project with Scrum Software Process Advanced Engineering and ICT-Convergence Proceedings (Vol.5, No.2), Jul. 2002
Ryeonggu Kwon, Gihwon Kwon, "FORMAL VERIFICATION OF STPA WITH MODEL CHECKING", European STAMP Workshop and Conference (ESWC 2022), Sep. 2022
장지영, 권기현, "Q-학습을 이용한 소코반 풀이에서 하이퍼-파라미터 분석", 한국정보기술학회논문지(20권 11호), 2022.11
조수희, 박소희, 권기현, "학생 친화적인 교육용 스크럼 프레임워크", 한국정보기술학회논문지(20권 11호), 2022.11
홍창기, 권기현, "강화학습 알고리즘 기반 실패 상태 도달 성능 비교", 한국정보기술학회 2022년도 추계종합학술대회 논문집 (17권 2호), 2022.12 [우수논문상(금상)]
박소희, 권령구, 권기현, "기계학습을 이용한 오픈소스 생존 가능성 예측", 한국정보기술학회논문지(20권 12호), 2022.12
Domestic Papers
「VDM을 사용한 정형적 명세의 동작 모형 구축」, 정보과학회논문지(22권 9호), pp.1334-1343, 1995.09. 한국정보과학회
「Map클래스의 설계 및 VDM 정형적 명세의 실행」, 정보과학회논문지(22권 10호), pp.1416-1424, 1995.10. 한국정보과학회
「Z 명세에서 객체 지향 구조 추출」, 정보처리학회 학술발표논문집(2권 2호), pp.288-291, 1995.10. 정보처리학회
「Z 명세의 객체 지향 애니메이션」, 정보과학회 학술발표논문집(22권 2호), pp.1363-1366, 1995.10. 정보과학회
「계약을 기반으로한 사용자 인터페이스 설계」, HCI '96학술대회 발표논문집(5권 1호), pp.137-142, 1996.02. 한국정보과학회
「C++를 위한 안전한 상속 가이드라인 확립」, 정보과학회 학술발표논문집(23권 1호), pp.615-618, 1996.04. 한국정보과학회
「상속이상에 대한 테스팅」, 정보과학회 학술발표논문집(23권 1호), pp.611-614, 1996.04. 한국정보과학회
「객체들간의 행위적 하위타입 관계 및 검증」, 소프트웨어공학회지(9권 3호), pp.3-16, 1996.09. 한국정보과학회 소프트웨어공학연구회
「클래스 계층구조에서 동적 행위의 호환성」, 정보과학회 학술발표논문집(23권 2호), pp.1465-1468, 1996.10. 한국정보과학회
「시제 논리를 이용한 객체의 동적 모델 합성」, 정보과학회 학술발표논문집(23권 2호), pp.1473-1476, 1996.10. 한국정보과학회
「객체지향 분석에서 동적 모델들의 일관성 검증」, 정보처리학회 학술발표논문집(23권 2호), pp.566-571, 1996.10. 정보처리학회
「Z 정형적 명세의 객체 지향 애니메이션」, 정보과학회논문지(B)(23권 12호), pp.1257-1269, 1996.12. 한국정보과학회
「동적 하위타입 관계의 정의 및 검증」, 인공지능연구회 학술발표논문집, pp.29-32, 1997.03. 한국정보과학회
「정리증명기를 이용한 요구명세의 자동확인」, '97인공지능연구회 학술발표논문집, pp.33-36, 1997.03. 한국정보과학회
「텀 개서에 의한 대수적 명세의 추론」, '97춘계학술발표논문집(4권 1호), pp.615-618, 1997.04. 한국정보처리학회
권기현 「정형 방법을 지원하는 정리증명기 개발」, '97봄 학술발표논문집(24권 1호), pp.591-594, 1997.04. 한국정보과학회
「자동정리 증명을 이용한 요구명세 검증」, '97춘계학술대회논문집, pp.183-189, 1997.06. 한국전문가시스템학회
「변환연산자에 의한 순서화」, 소프트웨어공학연구회 정형기법웍샵, pp.1-8, 1997.09. 한국정보과학회
「시제논리를 이용한 행위적인 하위타입관계의 정의 및 검증」, 한국정보과학회 논문집(24권 9호), pp.958-965, 1997.09. 한국정보과학회
「정형검증을 지원하는 정리증명기의 개발」, '97가을학술발표논문집(4권 2호), pp.717-722, 1997.10. 한국정보처리학회
「텀개서 시스템을 이용한 ACT ONE 대수적 명세의 검증」, '97가을학술발표논문집(24권 2호), pp.615-618, 1997.10. 한국정보과학회
「최우선 변환 연산자 비교에 의한 재귀적 순서」, '97학술발표논문집(24권 2호), pp.643-646, 1997.10. 한국정보과학회
「양상 뮤 논리를 위한 속성 명세 패턴」, 2001봄 학술발표논문집(A)(28권 1호), pp.598-600, 2001.04. 한국정보과학회
「기호적 기법을 이용한 상태도의 동치 검사」, 산학연 소프트웨어공학기술학술대회논문집, pp.214-219, 2001.05. 한국정보처리학회 소프트웨어공학연구회
「텀 개서 시스템을 이용한 상태도의 의미 정의 및 검증」, 정형기법 워크샵 논문집, pp.145-151, 2001.06. 정형기법연구회
「모형 검사를 위한 패턴기반의 시각적 속성 명세」, 소프트웨어공학기술 합동 워크샵 2001 발표집, pp.59-72, 2001.08. 한국정보과학회, 한국정보처리학회
「상태도의 정형 검증」, 제5차 통신전자정보화 학술대회, pp.303-308, 2001.09. 국방과학연구소
「계층 구조 기계의 도달성 검사」, 제5차 통신전자정보화 학술대회, pp.315-320, 2001.09. 국방과학연구소
「속성 명세를 위한 계층 시제 논리」, 소프트웨어공학연구회지(4권 3호), 2001.09. 한국정보처리학회 소프트웨어공학연구회
「속성 명세 지원 시스템」, 2001 가을 학술발표 논문집, 2001.10. 한국정보과학회
「계층형 크립키 구조에서 HiCTL 해석」, 한국정보과학회 프로그래밍언어논문지(15권 2호), pp.49-56, 2001.11. 한국정보과학회 프로그래밍언어연구회
「상태도의 의미 정의 및 SMV 코드로의 변환」, 한국소프트웨어공학회지, pp.49-61, 2001.12. 한국정보과학회 소프트웨어공학연구회
「정형 기법(Formal Method) Z」, 원자력 연구소, 2002.02. 원자력 연구소
「지정된 범위에서의 상태 불변식 생성」, 한국소프트웨어공학학술대회논문집(4권 4호), pp.309-314, 2002.03. 정보과학회
「상태 불변식의 투영」, 정보처리학회 춘계학술발표논문집(9권 1호), pp.415-418, 2002.04. 정보처리학회
「계층형 크립키 구조를 위한 CTL 모형검사 알고리즘」, 정보처리학회 춘계학술발표논문집(9권 1호), pp.407-410, 2002.04. 정보처리학회
「병행 기계를 이용한 상태도의 동치 검사」, 정보과학회 봄 학술발표논문집(29권 1호), pp.427-429, 2002.04. 정보과학회
「병행성을 이용한 상태도의 검증」, 정보처리학회 춘계학술발표논문집(9권 1호), pp.411-414, 2002.04. 정보처리학회
「Stepwise flattening and its application to model checking」, 소프트웨어공학논문지(5권 2호), pp.39-45, 2002.06. 정보처리학회
「범위에서의 상태 불변식 생성」, 소프트웨어 공학 회지(15권 2호), pp.49-57, 2002.06. 정보과학회 소프트웨어공학연구회
「계층형 명세 언어의 정의 및 검사」, 프로그래밍 언어 논문지(16권 2호), pp.5-14, 2002.07. 정보과학회 프로그래밍언어연구회
「Stepwise flattening and its application to model checking」, 소프트웨어공학 합동 워크샵, 2002.08. 정보과학회, 정보처리학회
「OCL을 이용한 상태 기계의 메타 모델링」, 정보과학회 가을 학술발표논문집(29권 2호), pp.37-39, 2002.10. 정보과학회
「만족성을 이용한 동치 검사」, 인터넷정보학회 추계학술발표논문집(3권 2호), pp.377-380, 2002.11. 인터넷정보학회
「자료 일치성을 위한 동기화 프로토콜의 정형 검증」, 정보처리학회 추계학술발표대회(9권 2호), pp.1973-1976, 2002.11. 정보처리학회
「모델 검증을 이용한 게임 풀이」, 정보과학회지(21권 1호), pp.7-14, 2003.01. 정보과학회
「모델 검사 기법을 이용한 게임 풀이」, 한국소프트웨어공학학술대회논문집(5권 1호), pp.60-76, 2003.02. 한국정보과학회
「행위적 메타 모델링을 위한 OCL의 확장」, 소프트웨어 공학 회지(16권 1호), pp.125-135, 2003.03. 한국정보과학회 소프트웨어공학연구회
「혼합 도달성 분석을 이용한 상태 불변식의 단순화」, 정보과학회 논문지, 2003.03. 정보과학회
「반례 생성을 위한 효율적인 기법」, 춘계학술대회논문집(4권 1호), pp.140-143, 2003.05. 한국인터넷정보학회
「NuSMV의 반례 생성 개선 및 게임 풀이에 적용」, 춘계학술발표대회 논문집, pp.101-105, 2003.06. 한국소프트웨어감정평가학회
「SMV를 이용한 유한 상태 기계의 동치 검사」, 정보과학회 논문지(30권 7호), pp.642-648, 2003.07. 한국정보과학회
「게임 풀이를 위한 NuSMV의 효율적인 반례 생성」, 정보처리학회논문지(10-D권 5호), pp.813-820, 2003.08. 한국정보처리학회
「K4 등급과 EAL3 등급의 호환성 검토에 관한 연구」, 소프트웨어공학 기술 합동 워크샵(3권 1호), pp.109-112, 2003.08. 한국정보과학회 한국정보처리학회 소프트웨어공학 연구회
「상태 공간의 저장 및 탐색 기법 비교」, 소프트웨어 공학 합동 워크샵(3권 1호), pp.113-119, 2003.08. 한국정보과학회 한국정보처리학회 소프트웨어공학 연구회
「NuSMV에서 생성된 반례길이 비교」, 학술발표논문집(II)(30권 2호), pp.358-360, 2003.10. 한국정보과학회
「모델 체킹에서의 상태 폭발 방지 기법」, 제1회 한일임베디드소프트웨어개발워크샵 튜토리얼 발표집, pp.47-77, 2003.11. 정보과학회소프트웨어공학연구회
「속성 분할을 이용한 릴레이 모델 체킹」, 프로그래밍언어논문지(17권 3호), pp.5-11, 2003.11. 한국정보과학회
「상태폭발을 방지하기 위해 속성분할을 이용한 사례들」, 추계학술발표대회 논문집(4권 2호), pp.449-452, 2003.11. 한국인터넷정보학회
「상태 폭발 문제 해결을 위한 릴레이 모델 체킹」, 한국소프트웨어공학학술대회논문집(6권 1호), pp.298-305, 2004.02. 한국정보과학회 소프트웨어공학연구회
「게임 풀이를 위한 상태공간축소」, 한국게임학회논문지(4권 1호), pp.58-66, 2004.03. 한국게임학회
「상태 폭발 문재 해결을 위한 릴레이 모델 체킹」, 소프트웨어공학회지(17권 1호), pp.25-33, 2004.03. 한국정보과학회 소프트웨어공학연구회
「모델 체킹에서 그래프 모양의 반례 생성」, 정보과학회 학술발표논문집(31권 1호), pp.352-354, 2004.04. 한국정보과학회
「모델 기반 임베디드 소프트웨어의 개발 경험」, 정보과학회 학술발표논문집(31권 1호), pp.400-402, 2004.04. 한국정보과학회
「다른 모델의 행위를 흉내내기」, 한국소프트웨어감정평가학회 춘계학술발표논문집, pp.35-40, 2004.05. 한국소프트웨어감정평가학회
「정보흐름 보안성에 대한 자바 바이트코드 검증」, 소프트웨어공학 합동워크샵(KSEJW-2004), pp.182-188, 2004.08. 소프트웨어공학연구회
「CC 기반 고등급 평가를 위한 보안정책 모델 작성방법」, 소프트웨어공학 합동워크샵(KSEJW-2004), pp.135-140, 2004.08. 소프트웨어공학연구회
「자바 바이트 코드에서 정보 흐름 보안성 검사」, 2004 가을 학술발표논문집(II)(31권 2호), pp.316-318, 2004.10. 한국정보과학회
「모델 체킹에서 상태 투영을 이용한 모델의 추상화」, 정보처리학회논문지 D(11-D권 6호), pp.1295-1300, 2004.10. 한국정보처리학회
「술어추상화를 이용한 자바 프로그램의 단순화 및 모델체킹」, 프로그래밍언어논문지(18권 3호), pp.37-44, 2004.11. 한국정보과학회 프로그래밍언어연구회
「술어 추상화를 이용한 자바 프로그램의 단순화」, 추계학술발표논문집, pp.61-65, 2004.11. 한국소프트웨어감정평가학회
「릴레이 모델 체킹을 이용한 상태 폭발 문제 해결」, 정보과학회논문지: 소프트웨어 및 응용(31권 11호), pp.1560-1567, 2004.11. 한국정보과학회
「임베디드 소프트웨어를 위한 코드 기반 모델 체킹 도구의 요구사항」, 추계학술발표대회 논문집(11권 2호), pp.327-330, 2004.11. 한국정보처리학회
「스마트카드 시스템을 위한 RBAC기반의 보안정책모델」, 추계학술발표대회 논문집(11권 2호), pp.331-334, 2004.11. 한국정보처리학회
「모델 체킹에서 안전성 위반에 대한 효율적인 반례 생성」, 정보처리학회논문지 D(12-D권 1호), pp.81-90, 2004.12. 한국정보처리학회논문지
「정형 기법의 국방 분야 적용 방안」, 제5회 국방 정보화기술 심포지움, pp.C-43-C-56, 2004.12. 한국국방연구원
「모델 체킹을 이용한 도망자-추적자 게임 풀이」, 한국게임학회 논문지(4권 2호), 2004.12. 한국게임학회
「레고 로봇을 위한 코드 자동생성 기법」, 한국소프트웨어공학학술대회논문집(1권 1호), pp.285-292, 2005.02. 한국정보과학회 소프트웨어공학연구회
「레고 로봇을 위한 코드자동생성기법」, 소프트웨어공학회지(18권 1호), pp.71-79, 2005.03. 한국정보과학회 소프트웨어공학연구회
「이진 프로그램을 위한 모델 체킹」, 소프트웨어공학회지(18권 2호), pp.35-42, 2005.06. 한국정보과학회 소프트웨어공학연구회
「임베디드 소프트웨어의 정형 검증」, 2005 Korea SEPG Conference, pp.1-22, 2005.06. 시스템통합기술원
「모델 체킹을 이용한 네모라이즈 게임 풀이」, 한국멀티미디어학회지(9권 2호), 2005.06. 한국멀티미디어학회
「이진 프로그램을 위한 CTL 모델 체킹」, 2005 한국 컴퓨터종합학술대회 논문집(32권 1호), pp.349-351, 2005.07. 한국정보과학회
「모델추상화를 이용한 네모라이즈 게임풀이」, 2005 한국 컴퓨터종합학술대회 논문집(32권 1호), pp.367-369, 2005.07. 한국정보과학회
「fFSM 모델의 정형 분석」, 프로그래밍언어논문지(19집 2권), pp.67-80, 2005.11. 한국정보과학회 프로그래밍언어연구회
「확장된 유한상태머신의 정형검증」, 2005 추계학술발표대회(6권 2호), pp.695-698, 2005.11. 한국인터넷정보과학회
「JAMES : 임베디드 자바 프로그램 모델체킹 도구」, 2005 추계학술발표대회(6권 2호), pp.217-222, 2005.11. 한국인터넷정보과학회
「모델 체킹을 위한 자바프로그램의 술어추상화」, 2005 가을학술발표논문집(32권 2호), pp.325-327, 2005.11. 한국정보과학회
「SMV를 이용한 확장된 유한상태머신의 정형검증」, 2005 가을학술발표논문집(32권 2호), pp.310-312, 2005.11. 한국정보과학회
「간단한 자바프로그램을 위한 CTL 모델 체킹」, 프로그래밍언어논문지(19집 2권), pp.47-66, 2005.11. 한국정보과학회 프로그래밍언어연구회
「임베디드 자바 프로그램의 정형 검증」, 정보처리학회논문지(12-D권 6호), 2005.12. 한국정보처리학회
「평탄화를 이용한 계층형 상태 기계의 단계 의미 정의」, 정보처리학회논문지, 2005.12. 한국정보처리학회
「효과적인 임베디드 소프트웨어 설계를 위한 제어흐름 모델의 자동 검증」, 정보처리학회논문지, 2005.12. 한국정보처리학회
「추상화를 통한 모델의 축소: 네모라이즈 게임 사례 연구」, 정보처리학회논문지(13-D권 1호), pp.111-116, 2006.02. 한국정보처리학회
「모델 체킹을 이용한 상태도 기반 소프트웨어 검증」, 2006 소프트웨어 공학 학술대회 논문집(8권 1호), pp.401-406, 2006.02. 한국정보과학회 소프트웨어공학연구회
「BOGOR의 성능 개선을 위한 범위 모델 체킹의 적용」, 2007 한국소프트웨어공학학술대회논문집(9권 1호), pp.394-403, 2007.02. 한국정보과학회 소프트웨어공학연구회
「마방진을 SMT 문제로 다루기」, 2007 한국소프트웨어공학학술대회논문집(9권 1호), pp.439-445, 2007.02. 한국정보과학회 소프트웨어공학연구회
「SAT Problem and Its Applications」, 한국소프트웨어공학학술대회 튜토리얼/초청강연, pp.3-16, 2007.02. 한국정보과학회 소프트웨어공학연구회
「자바 메모리 모델을 이용한 SAT 기반 멀티 스레드 자바 소프트웨어 검증」, 프로그래밍언어논문지(21권 1호), pp.1-10, 2007.04. 한국정보과학회 프로그래밍언어연구회
「예제를 통한 SAT 문제의 이해」, 한국IT서비스학회 2007 춘계학술대회, pp.1-18, 2007.05. 한국IT서비스학회
「Model Checking as a SAT Problem」, 2007년 소프트웨어공학연구회 단기강좌, pp.1-52, 2007.05. 한국정보과학회 소프트웨어공학연구회
「SAT 처리기를 위한 수도쿠 퍼즐의 최적화된 인코딩」, 정보과학회논문지(34권 7호), pp.616-624, 2007.07. 한국정보과학회
「LTS 바운드 모델 체킹」, 한국소프트웨어공학기술합동워크샵 2007발표집(5권 1호), pp.94-99, 2007.08. 한국정보과학회
「이진 서수 제약조건의 CNF 인코딩」, 한국소프트웨어공학기술합동워크샵 2007발표집(5권 1호), pp.100-107, 2007.08. 한국정보과학회
「BIR 모델의 바운디드 모델 검증」, 정보과학회논문지: 소프트웨어 및 응용(34권 8호), pp.743-751, 2007.08. 한국정보과학회
「정형 논리를 이용한 모델링 및 분석」, 정보과학회지(25권 11호), pp.16-25, 2007.11. 한국정보과학회
「다중 스레드 자바 프로그램의 SMT 기반 모델 검증」, 한국소프트웨어공학학술대회논문집(10권 1호), pp.451-458, 2008.02. 한국정보과학회 소프트웨어공학연구회
「이진 기수 조건에서 인접성 표현을 위한 최적화된 CNF 변환」, 한국소프트웨어공학학술대회논문집(10권 1호), pp.459-461, 2008.02. 한국정보과학회 소프트웨어공학연구회
「이진 변수 기수 조건을 위한 CNF 변환 방법의 분석」, 정보과학회논문지: 소프트웨어및응용(35권 2호), pp.81-90, 2008.02. 한국정보과학회
「자바 메모리 모델을 이용한 멀티 스레드 자바 코드 검증」, 정보처리학회논문지 D(15-D권 1호), pp.99-106, 2008.02. 한국정보처리학회
「모델 검증 도구를 이용한 극단 인터리빙 분석」, 소프트웨어공학회지(21권 1호), pp.3-12, 2008.03. 한국정보과학회 소프트웨어공학연구회
「미로 퍼즐 풀이를 통한 모델 체킹 도구의 특성 분석」, 춘계학술대회발표논문집(15권 1호), pp.382-385, 2008.05. 한국정보처리학회
「병행 프로그램에서 극단적 인터리빙의 정형 분석」, 춘계학술대회 발표논문집(15권 1호), pp.375-377, 2008.05. 한국정보처리학회
「SPIN의 효율적인 모델링 방법」, 춘계학술발표대회 발표논문집(9권 1호), pp.338-342, 2008.05. 한국인터넷정보학회
「지뢰찾기를 SAT 문제로 간주하기」, 춘계학술발표대회 발표논문집(9권 1호), pp.353-356, 2008.05. 한국인터넷정보학회
「LTS-BMC를 이용한 웹 서비스 검증」, 춘계학술발표대회 발표논문집(9권 1호), pp.363-367, 2008.05. 한국인터넷정보학회
「카운팅 문제에 대한 SAT, PB, SMT 의 성능 분석」, 춘계학술대회 발표논문집(15권 1호), pp.371-374, 2008.05. 한국정보처리학회
「SAT 사례 연구: 루빅 큐브」, 춘계학술대회 발표논문집(15권 1호), pp.378-381, 2008.05. 한국정보처리학회
「SPIN에서 마방진 풀이를 통한 데이터 추상화 이해」, 춘계학술발표대회 발표논문집, pp.83-88, 2008.06. 한국IT지적재산관리학회
「모델 체킹을 이용한 자바 기반 웹 서비스 검증」, 춘계학술발표대회 발표논문집, pp.77-82, 2008.06. 한국IT지적재산관리학회
「수도쿠 퍼즐을 통해서 살펴본 SAT에서 전처리 효과」, 한국IT서비스학회지(001719)(7권 2호), pp.127-135, 2008.06. 한국IT서비스학회
「SMT 를 이용한 자바 메모리 모델 시뮬레이션」, 2008 한국컴퓨터종합학술대회 발표논문집(35(A)권 1호), pp.72-73, 2008.06. 한국정보과학회
「모델 체킹을 이용한 JUnit 기반 테스트 드라이버 자동 생성」, 2008 한국컴퓨터종합학술대회 논문집(35(A)권 1호), pp.64-65, 2008.06. 한국정보과학회
「Promela 모델에 C 코드를 끼워서 추상화하기」, 2008 한국컴퓨터종합학술대회 발표논문집(35(B)권 1호), pp.86-88, 2008.06. 한국정보과학회
「웹서비스 설계와 구현의 일치성 검사」, 춘계학술발표대회 발표논문집, pp.71-76, 2008.06. 한국IT지적재산관리학회
「모델 체킹에서 하위 근사화 적용 경험」, 2008 한국 소프트웨어공학기술 합동 워크샵 논문집(6권 1호), pp.402-410, 2008.07. 한국정보과학회 한국정보처리학회
「병행성 분석을 위한 액션 기반의 LTS 바운드 모델 체커」, 정보과학회논문지(35권 9호), pp.529-537, 2008.09. 한국정보과학회
「이진 기수 조건에서 인접성 표현을 위한 최적화된 CNF 변환」, 정보과학회논문지 : 소프트웨어 및 응용(35권 11호), pp.661-670, 2008.11. 한국정보과학회
「Autosar Template 검증」, 제2차 차량 전장용 통합제어 SW 플랫폼 개발 워크샵 자료집, 2008.11. ETRI 융합소프트웨어연구본부 자동차융합기술 연구팀
「만족가능성 처리기를 이용한 이진 변수 서브시퀀스 추출」, 정보처리학회논문지D(15-D권 6호), pp.777-784, 2008.12. 한국정보처리학회
「모델 검증의 소개」, 시스템 보전,보증 정책 연구회 2008년도 WORKSHOP II, 2008.12. 한국신뢰성학회 시스템 보전,보증 정책 연구회
「SMT 해결기를 이용한 자바 메모리 모델 시뮬레이션」, 정보과학회논문지(15권 1호), pp.62-66, 2009.01. 한국정보과학회
「SMT를 이용한 UML 다이어그램 간의 일치성 검증」, 2009 한국 소프트웨어공학기술 합동 워크샵 논문집, 2009.07. 한국정보과학회, 한국정보처리학회
「ESC／Java2 를 위한 루프 불변 조건 제안」, 한국 소프트웨어공학 학술대회 논문집(12권 1호), pp.263-268, 2010.02. 한국정보과학회 소프트웨어공학소사이어티
「임베디드 소프트웨어에서 코드 리팩토링과 CBMC 모델 검증 도구의 적용」, 한국 소프트웨어공학 학술대회 논문집(12권 1호), pp.499-505, 2010.02. 한국정보과학회 소프트웨어공학소사이어티
「SMT Solver 를 이용한 프라임 경로 커버리지 기준을 만족하는 가능한 테스트 경로 찾기」, 한국 소프트웨어공학 학술대회 논문집(12권 1호), pp.289-296, 2010.02. 한국정보과학회 소프트웨어공학소사이어티
「웹 기반 시스템의 정형 검증」, 한국 소프트웨어공학 학술대회 논문집(12권 1호), pp.220-227, 2010.02. 한국정보과학회 소프트웨어공학 소사이어티
「AUTOCL 을 이용한 전장용 소프트웨어 Basic Software 의 구문 검사」, 한국 소프트웨어공학 학술대회 논문집(12권 1호), pp.234-239, 2010.02. 한국정보과학회 소프트웨어공학 소사이어티
「안전한 소프트웨어 개발을 위한 소스 코드 취약점 검사 도구의 개발」, 2010년 한국인터넷정보학회 학술발표대회 논문집(11권 1호), pp.255-256, 2010.06. 한국인터넷정보학회
「MC／DC 커버리지 측정 자동화 도구」, 2010년 한국인터넷정보학회 학술발표대회 논문집(11권 1호), pp.249-250, 2010.06. 한국인터넷정보학회
「CTL 모델 검증에서 논리식 폭발 문제 줄이기」, 2010년 한국인터넷정보학회 학술발표대회 논문집(11권 1호), pp.243-244, 2010.06. 한국인터넷정보학회
「안드로이드 애플리케이션 GUI 테스트」, 2010년 한국인터넷정보학회 학술발표대회 논문집(11권 1호), pp.253-254, 2010.06. 한국인터넷정보학회
「보안 코딩 가이드라인으로부터 취약점 자동검사 규칙의 구현」, 2010년 한국 소프트웨어공학기술 합동 워크샵 논문집(8권 1호), pp.118-122, 2010.08. 한국정보과학회 소프트웨어공학 소사이어티
「XPath 를 이용한 AUTOSAR BSW 모듈의 속성 검사」, 2010년 한국 소프트웨어공학기술 합동 워크샵 논문집(8권 1호), pp.216-225, 2010.08. 한국정보과학회 소프트웨어공학 소사이어티
「XPath 를 이용한 AUTOSAR Basic Software 모듈 설정 평가 도구 개발」, 소프트웨어공학소사이어티논문지(23권 3호), pp.85-97, 2010.09. 한국정보과학회
「LTL Synthesis를 통한 다중 로봇의 협업 계획」, 대한임베디드공학회 추계학술대회 논문집, 2010.11. 대한임베디드공학회
「AUTOSAR Basic Software 모듈의 설정을 평가하는 도구 개발」, 한국정보처리학회 추계학술발표대회 논문집(17권 2호), pp.299-302, 2010.11. 한국정보처리학회
「LTL Synthesis 를 통한 단일 로봇의 작업 계획」, 한국정보처리학회 추계학술발표대회 논문집(17권 2호), pp.295-298, 2010.11. 한국정보처리학회
「모델 검증을 통한 시스템의 반응형 작업 전략 찾기」, 대한임베디드공학회 추계학술대회 논문집, 2010.11. 대한임베디드공학회
「CBMC 모델 검증 도구를 이용한 엔터프라이즈 소프트웨어의 검증」, 한국 소프트웨어공학 학술대회 논문집(13권 1호), pp.179-185, 2011.02. 한국정보과학회 소프트웨어공학 소사이어티
「LTL Synthesis 를 이용한 반응형 시스템 디자인」, 한국 소프트웨어공학 학술대회 논문집(13권 1호), pp.155-162, 2011.02. 한국정보과학회 소프트웨어공학 소사이어티
「임베디드 소프트웨어에서 코드 리팩토링과 C 바운디드 모델 체커 도구의 적용」, 정보과학회논문지 : 소프트웨어 및 응용(38권 4호), pp.179-187, 2011.04. 한국정보과학회
「그래프 이론과 모델 기반의 안드로이드 GUI 테스팅」, 한국인터넷정보학회 하계학술발표대회 논문집(12권 1호), pp.317-318, 2011.06. 한국인터넷정보학회
「시나리오 기반 요구 사항으로부터 반응형 시스템 개발」, 한국인터넷정보학회 하계학술발표대회 논문집(12권 1호), pp.313-314, 2011.06. 한국인터넷정보학회
「시나리오 기반 명세 모델로부터 반응형 시스템 개발」, 한국컴퓨터종합학술대회 논문집(38권 1호), pp.200-203, 2011.06. 한국정보과학회
「LTL Synthesis와 그래프 커버리지를 이용한 GUI 테스트 경로 생성」, 한국컴퓨터종합학술대회 논문집(38권 1호), pp.217-220, 2011.06. 한국정보과학회
「시나리오 기반 명세 모델로부터 반응형 시스템 모델 개발」, 인터넷정보학회논문지(13권 1호), pp.99-106, 2012.02. 한국인터넷정보학회
「TMN 관리 기능을 이용한 USN 기반 데이터 통합운영관리시스템의 품질평가모델 개발」, 한국소프트웨어공학학술대회 논문집 (인터넷으로 배포), pp.1-8, 2012.02. 한국정보과학회
「LTL Synthesis를 이용하여 Live Sequence Charts로 부터 상태 차트 생성」, 한국소프트웨어공학학술대회 논문집 (인터넷으로 배포), pp.1-9, 2012.02. 한국정보과학회
「LTL Synthesis를 이용한 다중 로봇 시뮬레이터 개발」, 정보처리학회 춘계학술대회논문집(19권 1호), pp.1219-1222, 2012.04. 한국정보처리학회
「안드로이드 애플리케이션 GUI 테스팅 도구 적용 및 사례연구」, 정보처리학회 춘계학술대회논문집(19권 1호), pp.1231-1234, 2012.04. 한국정보처리학회
「GR(1) Synthesis를 이용한 퍼즐의 전략 찾기」, 한국컴퓨터종합학술대회 논문집(39권 1호), pp.147-149, 2012.06. 한국정보과학회
「상황 인식 시스템의 서비스 명세를 시제 논리로 표현하기」, 한국컴퓨터종합학술대회 논문집(39권 1호), pp.253-254, 2012.06. 한국정보과학회
「Mitigating the state explosion problem of synthesized multi-robot controller by decentralized model」, Proceedings of Korea-Japan Joint Workshop on ICT, pp.5-8, 2012.09. Information Processing Society of Japan ＆ Korean Institute of Information Scientists and Engineers
「정형기법을 이용하여 기능적으로 정확한 컨트롤러 개발 사례」, 추계학술발표대회 논문집(19권 2호), pp.1535-1538, 2012.11. 한국정보처리학회
「반응형 시스템을 위한 올바른 환경 모델의 생성」, 추계학술발표대회 논문집(19권 2호), pp.1543-1546, 2012.11. 한국정보처리학회
「레고 마인드스톰 NXT를 위한 센서 API 개선 사례」, 추계학술발표대회 논문집(19권 2호), pp.1559-1562, 2012.11. 한국정보처리학회
「SPIN과 SMV가 생성하는 반례의 특성 비교」, 추계학술발표대회 논문집(19권 2호), pp.1578-1580, 2012.11. 한국정보처리학회
「정형 기법을 이용한 테스트 오라클 생성」, 한국소프트웨어공학학술대회논문집(15권 1호), pp.190-198, 2013.01. 한국정보과학회
「합성 기법을 적용하여 로봇 컨트롤러를 개발하기 위한 로봇 제어 시스템 및 사례」, 정보과학회 종합학술대회 논문집, pp.580-582, 2013.06. 한국정보과학회
「JADE를 이용한 합성된 오토마타의 시뮬레이션」, 한국정보과학회 추계학술발표회 발표논문집, pp.542-544, 2013.11. 한국정보과학회
「에이전트 기반의 시뮬레이션을 통한 LTL 분산 명세의 확인」, 제16회 한국소프트웨어공학학술대회 논문집(16권 1호), pp.11-14, 2014.02. 한국정보과학회 소프트웨어공학 소사이어티
「JADE를 이용한 합성된 오토마타의 시뮬레이션 적용 사례」, 제16회 한국소프트웨어공학학술대회 논문집(16권 1호), pp.33-36, 2014.02. 한국정보과학회 소프트웨어공학 소사이어티
「난청 환자들을 위한 소음 훈련 시스템 개발에 관한 연구」, 2014년 춘계학술발표대회 논문집(21권 1호), pp.854-857, 2014.04. 한국정보처리학회
「상호 작용 중심 시스템의 품질 확보를 위한 LTL 분산 명세」, 정보처리학회논문지. 소프트웨어 및 데이터 공학(3권 5호), pp.169-178, 2014.05. 한국정보처리학회
「오토마타 생성 시간 단축을 위한 분산 명세 합성」, 2014 한국컴퓨터종합학술대회 논문집, pp.547-549, 2014.06. 한국정보과학회
「반응형 시스템 개발을 위한 안전-뷰키 게임의 구현 및 비교」, 한국소프트웨어공학학술대회 논문집(17권 1호), pp.380-381, 2015.01. 한국정보과학회 소프트웨어공학 소사이어티
「모델 검증과 모델 합성을 이용한 제어기 생성 사례 연구」, 2015년 한국컴퓨터종합학술대회 논문집, pp.1775-1777, 2015.06. 한국정보과학회
「오토마타 합성을 통한 청각장애인을 위한 위험방지 어플리케이션 개발」, 2015년 한국컴퓨터종합학술대회 논문집, pp.2031-2033, 2015.06. 한국정보과학회
「계층적 오토마타를 통한 드론 경로제어 」, 2015 한국컴퓨터종합학술대회 논문집, pp.1778-1780, 2015.06. 한국정보과학회
「민방위 경보음의 정형 명세에 관한 연구」, 2015년 추계학술발표대회 논문집(22권 2호), pp.1078-1079, 2015.10. 한국정보처리학회
「신호 시제 논리를 활용한 음악치료 시스템 개발」, 2015년 추계학술발표대회 논문집(22권 2호), pp.1080-1081, 2015.10. 한국정보처리학회
「신호 시제 논리를 사용한 순음 생성기 개발」, 2015년 추계학술발표대회 논문집(22권 2호), pp.1082-1084, 2015.10. 한국정보처리학회
「심전도 신호의 정형 명세」, 2015년 추계학술발표대회 논문집(22권 2호), pp.1085-1087, 2015.10. 한국정보처리학회
「A Unified Approach for UML Based Safety Oriented Level Crossing Using FTA and Model Checking」, 제19회한국소프트웨어공학학술대회 논문집(19권 1호), pp.89-96, 2017.02. 한국정보과학회, 한국정보처리학회
「안전 요구사항 추출을 위한 안전성 분석 지침 개발 및 적용 사례」, 제19회한국소프트웨어공학학술대회 논문집(19권 1호), pp.186-190, 2017.02. 한국정보과학회, 한국정보처리학회
「STAMP/STPA를 적용한 열차 소프트웨어 안전성 분석 사례」, 2017 한국소프트웨어종합학술대회 논문집, pp.607-609, 2017.12. 한국정보과학회
「안전한 소프트웨어 집약적 시스템을 위한 시스템 이론적 안전성 분석에서의 위험도 평가」, 제20회 한국소프트웨어공학 학술대회 논문집(20권 1호), pp.55-62, 2018.01. 한국정보과학회
「An Observation of Use Cases and Misuse Case in System Theoretic Process Analysis」, 제20회 한국 소프트웨어공학 학술대회 논문집(20권 1호), pp.84-91, 2018.01. 한국정보과학회
「IEC 61508 안전 무결성 수준의 정량적 검증」, 한국정보기술학회논문지(16권 9호), pp.43-50, 2018.09. 한국정보기술학회
「철도 시스템의 안전성 향상을 위한 하이브리드 위험원 분석」, 한국정보기술학회논문지(16권 11호), pp.133-144, 2018.11. 한국정보기술학회
「시나리오 테이블을 이용한 STPA에서의 사고 원인 식별」, 제21회 한국소프트웨어공학학술대회논문집(21권 1호), pp.18-19, 2019.01. 한국정보과학화
「시나리오 테이블을 이용한 STPA에서의 사고 원인 식별」, 정보과학회논문지(46권 8호), pp.787-799, 2019.08. 한국정보과학회
「소프트웨어 위험원 분석을 위한 상황 분류 기반의 조합을 통한 STPA 문맥표 최적화」, 제 22 회 한국 소프트웨어공학 학술대회 논문집(22권 1호), pp.66-75, 2020.02. 한국정보과학회
「결함 트리와 마코프 모델을 이용한 안전 기능의 정량적 검증」, 제 22 회 한국 소프트웨어공학 학술대회 논문집(22권 1호), pp.76-77, 2020.02. 한국정보과학회
「마코프 모델을 이용한 채팅 구성원 간의 관계 분석」, 한국정보기술학회논문지(18권 10호), pp.101-109, 2020.10. 한국정보기술학회
김소연, 권기현, "마코프 모델을 이용한 채팅 구성원 간의 관계 분석", 한국정보기술학회논문지(18권 10호), 2020.10
양현수, 권기현, "시나리오 테이블을 이용한 STPA에서의 사고 원인 식별", 한국정보과학회논문지(46권 8호), 2019.08
정대희, 권기현, "철도 시스템의 안전성 향상을 위한 하이브리드 위험원 분석(Hybrid Hazard Analysis for Improving Safety of Railway System)", 한국정보기술학회논문지 (16권11호), 2018.11
권기현, "IEC 61508 안전 무결성 수준의 정량적 검증 (Quantitative Verification of Safety Integrity Level in IEC 61508)", 한국정보기술학회논문지 (16권9호), 2018.09
International Papers
「Automatic Reasoning of Requirement Specifications」, Proc. the Workshop on Automated Proving, pp.39-48, 1997.07. Townsville, Australia
「Object-Oriented Animation of Z Specifications」, Proc. the Inter-Conference, pp.184-187, 1997.07. Artificial Intelligence&Soft Computing
「Equational Reasoning of Algebraic Specifications」, ISTED Inter-Conference, pp.129-132, 1997.11. Software Engineering(USA)
「Equational Reasoning System for Algebraic Specifications」, Proceedings of the ISSEE, pp.120-128, 1997.12. ISSEE(Korea)
「Automatic Verification of Requirement Specifications」, Proc. the Inter-Conference, pp.277-281, 1997.12. Intelligent Information System(Island)
「Validation of Algebraic Specifications」, Proceedings of Artificial Intelligence and Soft Computing, pp.102-105, 1998.05. IASTED
「Model Checking Basic Statecharts」, Proceedings of ICAI'00, 2000.06. International Conference Artifical Intelligence
「Model Checking Statecharts with Keeping Hierarchies」, Proceedings of FM-TOOLS 2000, pp.141-143, 2000.07. University Ulm
「Rewrite Rules and Operational Semantics for Model Checking UML Statecharts」, Lecture Notes in Computer Science, 2000.10. Springer Verlag
「CTL model checking algorithm for hierarchical Kripke structure」, International Conference on Computer and Information Science, pp.185-190, 2002.08. ACIS
「Generation of state invariant in scopes」, International Conference on Computer and Information Science, pp.203-208, 2002.08. ACIS
「Stepwise flattening for model checking」, Asian Pacific International Symposium on Internet and Multimedia, 2002.12. IITA, KIPS
「Applying Model Checking Techniques to Game Solving」, SERA'03, pp.88-93, 2003.06. ACIS
「LET'S PLAY MOBILE GAMES WITH MODEL CHECKING」, Proceedings of EALPIIT 2003, pp.203-208, 2003.07. National University of Mongolia
「Game Modeling and Its Optimizations」, Modeling, Simulation, and Optimization, pp.57-62, 2003.07. IASTED
「Formal Framework for Solving Box-Pushing Games」, SNPD'03, pp.309-314, 2003.10. International Association for Computer Information Science
「Applying Model Checking Techniques to Game Solving」, Lecture Notes in Computer Science(3026호), pp.290-303, 2003.12. Springer-Verlag
「Efficient Counterexample Generation for Solving Reachability Games」, Proceedings of SERA 2004, pp.8-13, 2004.05. ACIS
「Relay Model Checking for Solving The State Explosion Problem」, Proceedings of SERA 2004, pp.305-310, 2004.05. ACIS
「Solving Box-Pushing Games via Model Checking with Optimizations」, Lecture Notes in Computer Science 3299, pp.491-494, 2004.11. Springer
「Verification of UML-Based Security Policy Model」, Lecture Notes in Computer Science(3482호), pp.973-982, 2005.05. Springer
「Relay Reachability Algorithm for Exploring Huge State Space」, Proceedings of MoChArt' 2005, pp.17-27, 2005.08. Program Organizer of MoChArt
「Handling State Explosion in Model Checking」, International Workshop on Future Software Technology 2005, 2005.11. Software Engineers Association
「Model Checking for Simple Java Programs」, International Workshop on Future Software Technology 2005, 2005.11. Software Engineers Association
「Formal Verification of fFSM Model」, International Workshop on Future Software Technology 2005, 2005.11. Software Engineers Association
「Formalization of fFSM Model and Its Verification」, Lecture Notes in Computer Science(3820호), pp.361-372, 2005.12. Springer
「Relay Model Checking Algorithm for Searching Huge State Space」, Electronic Notes in Theoretical Computer Science(149권 2호), pp.19-31, 2006.01. Elsevier
「Avoidance of State Explosion Using Dependency Analysis in Model Checking Control Flow Model」, Lecture Notes in Computer Science(3984호), pp.905-911, 2006.05. Springer
「CTL Model Checking for Boolean Program」, Lecture Notes in Computer Science(3984호), pp.1081-1089, 2006.05. Springer
「Optimized CNF Encoding for Sudoku Puzzles」, Proceedings of LPAR 2006, pp.1-5, 2006.11. LPAR
「Efficient CNF Encoding for Selecting 1 from N Objects」, Proceedings on the worskhop CFV'07, pp.1-10, 2007.07. CADE-21
「SAT Based Verification Tool for Labeled Transition System」, Procedding of SERA 2007, pp.221-226, 2007.08. IEEE Computer Society
「Using Bounded Model Checking with BOGOR」, Proceeding of SERA 2007, pp.863-868, 2007.08. IEEE Computer Society
「Bounded Model Checking for Labeled Transition System」, Proceedings of JWSD 2007, pp.1-6, 2007.10. 한국정보과학회, 일본소프트웨어공학협회
「Using Boolean Cardinality Constraint for LTS Bounded Model Checking」, Proceedings of SEKE 2008, pp.537-542, 2008.07. Knowledge Systems Institute Graduate School
「Japanese Puzzle as a SAT Problem」, Proceedings of SEKE 2008, pp.543-548, 2008.07. 1. Knowledge Systems Institute Graduate School
「SMT-based Verification for Multithreaded Java with Java Memory Model」, Proceedings of the 8th APIS, pp.225-228, 2009.01. University of Ryukyus
「Under Approximation Refinement with SPIN Model Checker」, Proceedings of the 8th APIS, pp.275-278, 2009.01. University of Ryukyus
「Checking Well-Formedness Rules of AUTOSAR Model」, Proceedings of the 8th APIS, pp.503-506, 2009.01. University of Ryukyus
「Formal Verification of UML2.0 Sequence Diagram」, Proceedings of International Conference on Software Engineering and Knowledge Engineering, 2010.07. Knowledge Systems Institute
「OCL Evaluation on AUTOSAR Model」, Proceedings of International Conference on Software Engineering and Knowledge Engineering, 2010.07. Knowledge Systems Institute
「Effective feasible test path generation for Prime Path Coverage Criteria」, Proceedings of International Conference on Internet, pp.413-417, 2010.12. Korean Society for Internet Information
「Generating Test Requirements for MC／DC Coverage with AST」, Proceedings of International Conference on Internet, pp.419-423, 2010.12. Korean Society for Internet Information
「Applying Lightweight Formal Approach to Automatic Configuration Inspection」, Proceedings of International Conference on Software Engineering ＆ Knowledge Engineering, pp.107-110, 2011.07. Knowledge System Institute
「Extracting a Winning Strategy in a Game: A Case Study of Theseus and Minotaur」, Proceedings of CNSI 2012, pp.325-329, 2012.07. Institute of Information Science and Technology
「Collaborative Multi-Robot Simulation using LTL Synthesis」, Proceedings of CNSI 2012, pp.462-467, 2012.07. Institute of Information Science and Technology
「Get-Me-Out Puzzle as One Player Reachability Game」, Lecture Notes in Electrical Engineering(164호), pp.669-673, 2012.06. Springer Verlag
「Simulation of Collaborative Multi-robots」, Communications in Computer and Information Science, pp.588-593, 2012.08. Springer Verlag
「Automatic Construction of Test Oracle via Synthesis 」, Proceedinds of Computer Applications and Information Processing, pp.217-220, 2013.06. Korea Information Pocessing Society
「Parallel Execution of Models in GR(1) Synthesis」, Proceedins of ICT 2013, pp.1-3, 2013.12. Japan Information Processing Society
「Multi-Robot Collaboration Simulation Using LTL Synthesis」, Information(17권 5호), pp.1763-1769, 2014.05. International Information Institute
「State Minimization of Synthesized Finite State Machine」, Proceedings of The 5th International Conference on Convergence Technology 2015(5권 1호), pp.41-42, 2015.06. Korea Convergence Society
「Case Study of Synthesizing Automata from Message Sequence Chart」, Proceedings of The 5th International Conference on Convergence Technology 2015(5권 1호), pp.43-44, 2015.06. Korea Convergence Society
「Synthesizing Speaker Controller in Localization Training System for Hearing Impairment」, Proceedings of The 5th International Conference on Convergence Technology 2015(5권 1호), pp.133-134, 2015.06. Korea Convergence Society
「FORMAL VERIFICATION APPROACH FOR THE INTER-PARTITION COMMUNICATION OF ARINC 653 BASED KERNEL」, ICIC Express Letters(9권 5호), pp.1291-1296, 2015.05. ICIC Express Letters Office
「A Case Study of Hierarchical Safety Analysis for Eliciting Traceable Safety Requirements」, Lecture Notes in Electrical Engineering(448집), pp.474-480, 2017.05. Springer Verlag
「Failure Analysis in Safety Critical Systems Using Failure State Machine」, Lecture Notes in Electrical Engineering(474집), pp.540-545, 2017.12. Springer Verlag
「An Extended Hierarchical Safety Analysis for Software-Intensive System」, Lecture Notes in Electrical Engineering(474집), pp.1250-1256, 2017.12. Springer Verlag
「Reliability and Control Theory: An Integration Approach for Safety Analysis」, Lecture Notes in Electrical Engineering(474집), pp.1244-1249, 2017.12. Springer Verlag
「Comparing the Effectiveness of SFMEA and STPA in Software-Intensive Railway Level Crossing System」, Lecture Notes in Electrical Engineering(474집), pp.1281-1288, 2017.12. Springer Verlag