소프트웨어 분석 연구실 (Software Analysis Laboratory)

소프트웨어 분석 연구실은 안전하고 신뢰할만한 소프트웨어를 만드는 기술을 연구합니다. 본 연구실은 프로그래밍 언어에 대한 이해를 바탕으로 SW 자동 분석 및 검증 기술, SW 자동 패치 기술, SW 자동 합성 기술을 연구하고 있으며 학술적으로는 소프트웨어 분야 최상위 학술대회 및 학술지에 연구 성과를 발표함과 동시에 국내외 기업과 연계하여 실제 문제 해결에 이바지하는 노력을 기울이고 있습니다.
또한 본 연구실은 SW보안 국제공동연구센터 (CSSA)에 소속되어 소프트웨어 보안을 위한 프로그램 분석 기술을 연구개발하고 있습니다.

Research Areas

We research on fundamental technologies for software analysis, including

• Static and dynamic program analysis 정적/동적 프로그램 분석
• Formal program verification 엄밀한 프로그램 검증
• Program synthesis 프로그램 자동 합성
• Program repair 프로그램 자동 수정
• Software security 소프트웨어 보안

Current Research Topics

• 기계학습 기반 고성능 소프트웨어 분석 기술
  
  참고 논문:
  • Data-Driven Context-Sensitivity for Points-to Analysis
    Sehun Jeong*, Minseok Jeon*, Sungdeok Cha, and Hakjoo Oh (*contributed equally)
    OOPSLA 2017: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications
    [pdf] [link] [slides] [poster]
  • Automatically Generating Search Heuristics for Concolic Testing
    Sooyoung Cha, Seongjoon Hong, Junhee Lee, and Hakjoo Oh
    ICSE 2018: International Conference on Software Engineering
    [pdf] [tool]


• 프로그램 오류 및 보안 취약점 자동 패치
  
  참고 논문:
  • MemFix: Static Analysis-Based Repair of Memory Deallocation Errors for C
    Junhee Lee*, Seongjoon Hong*, and Hakjoo Oh (*contributed equally)
    FSE 2018: ACM SIGSOFT Symposium on the Foundations of Software Engineering (accepted)
    [pdf] [tool]
  • Automatic Diagnosis and Correction of Logical Errors for Functional Programming Assignments
    Junho Lee, Dowon Song, Sunbeom So, and Hakjoo Oh
    OOPSLA 2018: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (accepted)
    [pdf]
  
  
• 프로그램 자동 완성 소프트웨어
  
  참고 논문:
  • Synthesizing Pattern Programs from Examples
    Sunbeom So and Hakjoo Oh
    IJCAI 2018: International Joint Conference on Artificial Intelligence
    [pdf]
  • Synthesizing Imperative Programs from Examples Guided by Static Analysis
    Sunbeom So, Hakjoo Oh
    SAS 2017: Static Analysis Symposium
    [pdf] [tool]


• 스마트 컨트랙트 보안 취약점 검증

Introduction to our research

• Introduction to our research (2018.06)
• 소프트웨어 오류 자동 수정 기법 (2018.06)
• Data-Driven Static Analysis (2017.09)
• Static Analysis Research at Korea University (2016.06)
• 고성능 정적 프로그램 분석 기법 (정보과학회지 34권 3호)
• 프로그램 자동 생성 기술 (정보과학회 뉴스레터)
• 학부 졸업프로젝트 주제들
• 함수형 프로그램 자동수정 (2017.06)
• 명령형 프로그램 자동합성 (2016.12)
• 정규표현식 자동합성 (2016.06)
• Enough to check Collatz Conjecture for 16k+11

Software Releases

• Sparrow: A static analyzer for C programs (Commercial product)
  
• ParaDySe: A tool for automatically generating search heuristics for concolic testing
• ConTest: A concolic testing tool that adaptively reduces search space
• Simpl: A program synthesizer for imperative programs
• AlphaRegex: A regular expression synthesizer