[차수영 교수] 소프트웨어분석연구실(SAL), ICSE 2025 논문 게재 승인

소프트웨어 분석 연구실 (지도교수: 차수영)의 이재혁 학생 (석사과정)의 논문이 소프트웨어공학 분야 최우수 학회인 ICSE 2024 (IEEE/ACM International Conference on Software Engineering)에 게재 승인(Accept) 되었습니다. 해당 논문은 2025년 4월에 캐나다 Ottawa에서 발표될 예정입니다.

본 논문 "TopSeed: Learning Seed Selection Strategies for Symbolic Execution from Scratch"은 대표적인 소프트웨어 테스팅 방법 “기호 실행(Symbolic Execution)”의 성능을 높이기 위해, 사전 지식 없이 좋은 “시드(Seed)”를 선택하는 전략을 제안한다. 기호 실행에서 “시드”는 비싼 SMT 풀이 비용 없이, 테스트할 프로그램의 코드를 효과적으로 탐험할 수 있도록 도움을 주는 역할을 한다. 그러나, 대부분의 최신 기호실행 기술들은 시드를 사용하지 않고 그 성능을 높이는데 초점을 맞추었다. 본 논문에서는 다양한 최신 기호 실행 기술들이 사전 지식 없이 좋은 시드를 선택할 수 있도록 도와주는 상호 보완적인 방법인 TopSeed를 제안한다. 실험적으로, TopSeed는 다수의 오픈소스-C 프로그램들에 대해 다양한 최신 기호 실행 기술들의 성능을 분기 커버리지(Branch Coverage)와 오류 검출 관점에서 크게 향상시키는데 성공하였다.

[논문 정보]

• 제목: TopSeed: Learning Seed Selection Strategies for Symbolic Execution from Scratch
• 저자: 이재혁, 차수영
• 학회: IEEE/ACM International Conference on Software Engineering (ICSE 2025)
• 
  

Abstract:

We present TopSeed, a new approach that automatically selects optimal seeds to enhance symbolic execution. Recently, the performance of symbolic execution has significantly improved through various state-of-the-art techniques, including search strategies and state-pruning heuristics. However, these techniques have typically demonstrated their effectiveness without considering “seeding”, which efficiently initializes program states for exploration. This paper aims to select valuable seeds from candidate inputs generated during interactions with any symbolic execution technique, without the need for a predefined seed corpus, thereby maximizing the technique's effectiveness. One major challenge is the vast number of candidates, making it difficult to identify promising seeds. To address this, we introduce a customized online learning algorithm that iteratively groups candidate inputs, ranks each group, and selects a seed from the top-ranked group based on data accumulated during symbolic execution. Experimental results on 17 open-source C programs show that TopSeed significantly enhances four distinct cutting-edge techniques, implemented on top of two symbolic executors, in terms of branch coverage and bug-finding abilities.