연구 영역

대표 연구 분야

연구실에서 최근에 진행되고 있는 관심 연구 분야

1

프로그램 합성(Program Synthesis)

프로그램 합성은 사용자의 요구 조건이나 입출력 예제 등 명세를 바탕으로, 자동으로 프로그램을 생성하는 기술입니다. 이 분야는 소프트웨어 개발 생산성 향상, 프로그래밍 교육, 프로그램 최적화 등 다양한 응용 분야에서 큰 잠재력을 가지고 있습니다. 특히, 최근에는 대형 언어 모델(LLM)과 결합하여 더욱 복잡하고 대규모의 프로그램을 자동으로 생성하는 연구가 활발히 이루어지고 있습니다. 프로그래밍 시스템 연구실에서는 다양한 프로그램 합성 기법을 개발하고 있습니다. 예를 들어, 예제 기반 합성, 구문 유도 합성(Syntax-guided Synthesis), 확률 모델을 활용한 탐색 가속화, 재귀호출 함수 합성, 타입 기반 합성, 신경-기호적 합성 등 다양한 접근법을 통해 합성의 정확도와 효율성을 높이고 있습니다. 또한, 프로그램 합성 과정에서 발생하는 탐색 공간의 크기 문제를 해결하기 위해 분할 정복, 요약 해석, 버전 스페이스 학습 등 첨단 알고리즘을 적용하고 있습니다. 이러한 연구는 실제로 다양한 소프트웨어 개발 현장에 적용되고 있으며, 자동 코드 생성, 프로그램 최적화, 오류 자동 수정 등 실질적인 성과로 이어지고 있습니다. 앞으로도 프로그램 합성 기술은 인공지능 기반 소프트웨어 개발의 핵심 동력으로 자리매김할 것으로 기대됩니다.

2

정적 프로그램 분석 및 소프트웨어 품질 관리

정적 프로그램 분석은 프로그램을 실제로 실행하지 않고, 소스 코드만을 분석하여 오류, 보안 취약점, 성능 문제 등을 사전에 탐지하는 기술입니다. 이 연구실에서는 정적 분석의 정확도와 확장성을 동시에 달성하기 위한 다양한 이론적·실용적 방법론을 연구하고 있습니다. 대표적으로 데이터플로우 분석, 포인터 분석, 타입 시스템, 추상 해석(abstract interpretation) 등 다양한 분석 기법을 개발 및 적용하고 있습니다. 특히, 대규모 소프트웨어의 분석 효율성을 높이기 위해 희소 분석(sparse analysis), 알람 클러스터링, 진행도 표시(progress indicator) 등 실용적인 도구와 알고리즘을 개발하였으며, 클라우드 환경에서의 안전한 분석(static analysis-as-a-service in secrecy)과 암호화된 코드 분석 등 보안성을 강화한 분석 프로토콜도 연구하고 있습니다. 또한, 소프트웨어 테스팅, 자동화된 테스트 케이스 생성, 랜덤 테스팅, 델타 디버깅 등 소프트웨어 품질 향상을 위한 다양한 자동화 기법도 함께 다루고 있습니다. 이러한 연구는 실제 상용 소프트웨어 개발 및 유지보수 과정에서 품질과 신뢰성을 높이는 데 크게 기여하고 있습니다. 정적 분석 및 품질 관리 기술은 소프트웨어의 복잡성이 증가하는 현대 개발 환경에서 필수적인 요소로, 앞으로도 지속적으로 발전할 전망입니다.

3

프로그램 최적화 및 보안: 합성과 분석의 융합

프로그래밍 시스템 연구실에서는 프로그램 합성과 정적 분석 기술을 융합하여, 프로그램의 성능 최적화와 보안성 강화를 위한 혁신적인 연구를 수행하고 있습니다. 예를 들어, 동형암호(Fully Homomorphic Encryption) 회로의 최적화, 난독화된 프로그램의 역난독화, 프로그램 디블로팅(debloating) 등 다양한 응용 분야에서 프로그램 합성과 분석 기법을 결합하여 새로운 해결책을 제시하고 있습니다. 특히, 프로그램 합성을 활용한 자동 최적화 규칙 학습, 텀 다시쓰기(term rewriting), 등가 변환 학습 등은 기존의 수작업 기반 최적화 기법의 한계를 극복하고, 복잡한 프로그램 구조에서도 효율적이고 안전한 최적화를 가능하게 합니다. 또한, 악성코드 탐지 및 분석, 암호화된 코드의 안전한 분석 등 보안 분야에서도 프로그램 합성과 정적 분석의 융합이 중요한 역할을 하고 있습니다. 이러한 연구는 실제로 다양한 산업 현장과 오픈소스 커뮤니티에서 활용되고 있으며, 소프트웨어의 성능과 보안성을 동시에 향상시키는 데 큰 기여를 하고 있습니다. 앞으로도 프로그램 합성과 분석의 융합 연구는 소프트웨어 공학의 새로운 패러다임을 제시할 것으로 기대됩니다.