머신러닝 소프트웨어를 위한 자동화 테스팅 기술

  머신러닝 기술을 사용하여 인공지능 시스템을 구축하는 데 관심이 증가함에 따라 머신러닝 알고리즘을 쉽게 통합 할 수 있도록 Tensorflow, PyTorch 등 다양한 라이브러리가 출시되었다. 이런 라이브러리도 다른 소프트웨어 처럼 수많은 버그가 포함돼 있으며 해당 버그는 머신러닝 모델의 정확성과 성능에도 영향을 미친다. 따라서 머신러닝 소프트웨어의 더 나은 안정성을 위해 자동화 테스팅의 필요성이 대두되고 있지만, 머신러닝 라이브러리 함수 중 상당수가 특정 제약 조건을 따르는 구조화 된 입력값을 기대하기 때문에 기존 테스팅 연구 방법으로는 머신러닝 소프트웨어를 효과적으로 테스트 할 수 없다. 본 세미나에서는 API 문서에서 함수 제약 조건을 추론하고 잘못된 테스트 입력값을 분류하여 이 문제를 해결하는 테스팅 접근 방식을 제시한다.

- 2021.03. ~ 현재 : 울산과학기술원 조교수
- Purdue University 박사후연구원
- Hong Kong University of Science and Technology, 컴퓨터공학과, 박사
- Georgia Institute of Technology, 컴퓨터과학과, 석사
- University of Illinois at Urbana Champaign, 컴퓨터과학과, 학사

연구분야: Software Testing, Software Security, Empirical Study

SW 가시화를 위한 메타모델과 모델변환

  고품질의 SW 개발은 소스 코드와 개발 프로세스에 대한 지속적인 관리가 필요하다. CMMi, SP와 같은 프로세스 인증은 고품질 SW 개발의 전통적인 방법이다. 그러나 수작업을 통한 SW 프로세스의 품질관리 수행은 많은 인력과 자원이 소모된다. SW 가시화(Visualization)는 수작업 관리의 방안의 대안로 프로세스, 아키텍처, 문서를 시각화하고 자동화한다. 가시화는 역공학 기법을 통해 SW 개발의 가장 어려운 점인 SW 비가시성을 극복함으로써 SW 개발의 전체 과정을 파악하며, 이를 통하여 SW 품질을 측정하고 관리한다. 그러나 SW 가시화를 구축하기 위해서는 이종의 도구들의 통합이 필요하다. 본 발표에서는 SW 가시화를 실현하기 위한 모델 변환과 메타 모델에 대해서 소개한다. 모델 변환 및 메타모델은 이종의 데이터와 플랫폼을 연결하기 위한 방법으로 SW 가시화와 같이 이종의 플랫폼을 이용한 시스템 통합에 필요한 기술이다. 본 발표는 메타모델의 기본적인 설계 방법과 모델 변환에 대한 자세한 기술을 설명할 것이고 이를 활용한 SW 가시화 응용 사례들을 살펴볼 것이다.

- 2021.03 ~ 현재 : 목포대학교 컴퓨터공학과 조교수
- 2017.10 ~ 2021.02. : (주)모아소프트 SBAS 사업부 책임연구원
- 2015.09 ~ 2017.12. : 선문대학교 IT교육학부 시간강사
- 2009.02 ~ 2015.08. : 홍익대학교 전자전산공학과 박사 (지도교수: 김영철)
- 2007.03 ~ 2009.02. : 홍익대학교 전자전산공학과 석사 (지도교수: 김영철)
- 1999.03 ~ 2007.02. : 홍익대학교 컴퓨터정보통신공학과 학사

연구분야: 메타모델, 모델변환, 테스팅 자동화, 소프트웨어 품질 관리

A Robust Foundation for the Correctness of LLVM Compiler

  Intermediate representation (IR) is a language that is used internally by a compiler to represent programs. Translation to an IR should preserve guarantees from the source language's specification because they enable various optimizations. This naturally makes an IR a language that is rich with high-level information. In LLVM, the semantics of important high-level features in IR was not rigorously defined. It caused compiler optimizations in LLVM to use different interpretations, and bad interactions between the optimizations resulted in miscompilation bugs that are hard to fix. To solve this problem, the IR’s semantics must be defined precisely. Then, optimizations that are incorrect with respect to the chosen semantics must be fixed. Both processes are challenging because LLVM is a large, fastly evolving software.
This talk proposes (1) formal semantics of LLVM IR that resolves critical problems that we have found in the old IR semantics, making it consistent (2) a translation validation framework for LLVM's optimizations to validate the new semantics. We show that the old semantics of undefined behavior and memory model in the IR cannot explain important optimizations in LLVM. We propose new semantics that solves this problem. Next, we present Alive2, a translation validation framework for LLVM based on the new semantics. Alive2 relies on an automatic theorem prover to validate optimizations without any hints from LLVM. It supports most of integer and float operations, memory operations, function calls, and branches. To make validation practical, resources used by the tool is bounded.
The new formal semantics of undefined behavior has been adopted by LLVM. The `freeze' instruction that is proposed by us is officially added into LLVM 10.0, and the official document is updated to use our semantics. Also, critical problems in the old memory model we have found were shared with compiler developers, and patches have landed in LLVM to fix it. Alive2 has found more than 50 miscompilation bugs in LLVM so far and is used daily by LLVM developers.

  Juneyoung Lee received Ph.D. in Computer Science and Engineering from Seoul National University in 2021, and B.S. from Computer Science and Engineering from POSTECH in 2014. His research interests are the formal semantics of real-world programming languages and compiler verification. He is a recipient of the Distinguished Paper Award of PLDI'21. He actively worked as a contributor of the LLVM project, an open-source compiler infrastructure. Many compilers -- Clang (Apple's C/C++ compiler), NVIDIA's CUDA compiler, Intel's ICC, Swift, Rust -- rely on LLVM to perform compiler optimizations and generate code to various targets. He was a keynote speaker of 2020 LLVM Developers' Meeting, which is one of two seminal conferences for LLVM developers. Also, he actively contributed to Alive2, an automatic validation framework for compiler optimizations. Alive2 mathematically proves that a given compiler transformation is correct. The Alive2 online is daily used in the code review process of the LLVM project. He is currently working for CryptoLab as a military service agent. CryptoLab is a company developing a fast homomorphic encryption framework and post-quantum cryptography library.

오픈소스 소프트웨어에서의 버그 정정 관리를 위한 지능형 프레임워크

  소프트웨어의 복잡성 증가로 소프트웨어 유지보수에서 디버깅의 비용이 약 610억 달러 (연간)의 비용이 소요되고 있으며 시간으로 환산하면 약 6억 2천만의 개발자 시간이 소프트웨어 디버깅에 소요되고 있다. 만약 자동화된 소프트웨어 버그 정정 프레임워크가 존재한다면 개발자의 디버깅 시간을 줄여 개발 생산성을 확보할 수 있고 소프트웨어 유지보수의 비용을 줄일 수 있다. 본 발표에서는 오픈소스 소프트웨어에서의 버그 정정 관리를 위한 지능형 프레임워크를 소개한다. 소프트웨어 버그 심각도 예측, 소프트웨어 버그 개발자 추천, 소프트웨어 버그 로컬라이제이션, 소프트웨어 버그 정정을 하나의 프레임워크를 통합하여 소프트웨어 유지보수를 효율적으로 할 수 있는 방법을 살펴본다.

- 2021.03 ~ 현재 : 조교수, 컴퓨터공학부, 경남대학교
- 2020.09 ~ 2021.02. : 연구교수, 서울시립대학교
- 2017.12 ~ 2020.08. : AI 개발자, KB국민은행(본부)
- 2016.02 ~ 2017.07. : AI 개발자, MBC문화방송사(본사)
- 2015.02 ~ 2016.01. : SW 개발자, 서울신문사(본사)
- 2016.02 ~ 2020.08. : 박사, 컴퓨터과학과, 서울시립대학교
- 2013.03 ~ 2015.02. : 석사, 컴퓨터과학과, 서울시립대학교
- 2006.03 ~ 2013.02. : 학사, 컴퓨터공학부, 한국기술교육대학교

비형식 요구사항 기반 유스케이스 추출을 통한 노력 추정 방법

  고품질 소프트웨어를 개발하기 위해서는 소프트웨어 개발 초기 단계에서 요구 사항에 대한 정확한 분석이 필요하다. 그러나 대부분의 자연어 위주의 비형식 요구 사항은 분석이 어렵다. 이러한 문제를 해결하기 위해, 자연어로 작성된 비형식 요구사항에서 유스케이스 추출 방법을 제안한다. 자연어 요구 사항을 이해하기 위해 Fillmore의 격문법(Case Theory)을 개선했다. 제안하는 방법은 개선된 격문법을 통해 자연어 요구 사항을 분류하고 구문 분석을 통해 문장의 구조와 관계를 식별하기 위해 요구 사항을 분석한다. 이 정보에서 동사를 나열하고 주동사를 추출한다. 8개의 개선된 사례를 기반으로 한 문장의 인수를 요구사항으로 분석한다. 분석된 정보는 시각적 모델링, 즉 변환된 모델을 통해 유스케이스를 추출한다. 마지막으로 추출된 유스케이스를 기반으로 소프트웨어 노력 추정을 계산한다. 이 방법은 이해 관계자가 쉽게 이해할 수 있도록 처리할 수 있는 자연어 요구 사항을 수정하지 않고 유스 케이스를 추출할 수 있다. 또한 유스케이스 점수(Usecase Point) 기법을 기반으로 소프트웨어 노력을 추정할 수 있다.

- 2021.08. ~ 현재 : 진주교육대학교 컴퓨터교육과 조교수
- 2021.03. ~ 2021.08. : 유원대학교 스마트IT학과 조교수
- 2020.08. : 홍익대학교 일반대학원 소프트웨어공학(박사)
- 2012.08. : 홍익대학교 일반대학원 소프트웨어공학(석사)
- 2008.02. : 홍익대학교 컴퓨터정보통신(학사)

연구분야: 요구공학, 소프트웨어 가시화, 저전력 및 성능 가시화, AI 기반 소프트웨어 개발 방법론, 컴퓨터교육

소프트웨어 신뢰도 보증을 위한 효율적인 도달 가능성 분석

  도달 가능성 분석은 프로그램이 안전하지 않은 상태 (e.g., 에러 위치)에 도달할 수 없다는 것을 증명함으로써 소프트웨어의 신뢰도를 보증하는 방법이다. 그런데 모델 체킹과 같은 자동화된 분석 방법이 있음에도 불구하고 프로그램의 높은 복잡도로 인하여 최신의 기법조차 너무 긴 분석시간을 소모하거나 혹은 도달 가능성 분석에 실패하곤 한다. 본 발표에서는 도달 가능성 분석을 위한 최신 기법들과 그 기법들의 문제점을 소개하고 기존 기법들의 속도를 향상시킨 TOUR를 소개한다. TOUR는 도달 가능성 분석을 위한 최신 기법인 추상 도달가능성 기반 모델 체킹 (ARMC)에 에러 위치 지향 탐색 전략을 적용함으로써 분석 속도를 향상 시킨다. TOUR를 적용한 결과 652개의 복잡한 프로그램들을 대상으로 기존 ARMC 기법보다 15%많은 프로그램들을 15% 적은 시간만에 분석하여 속도가 향상된 것을 확인 하였다.

- 2022.01. ~ 현재 : 한양대학교 산학협력단 박사후 연구원
- 2015.03. ~ 2022.02. : 한국과학기술원 전산학부 박사
- 2013.03. ~ 2015.02. : 한국과학기술원 전산학부 석사
- 2006.03. ~ 2013.02. : 건국대학교 컴퓨터공학부 학사

연구분야: 소프트웨어 검증, 소프트웨어 모델 체킹, 소프트웨어 시험, 소프트웨어 신뢰성 공학