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

본 논문 "Enhancing Symbolic Execution with Self-Configuring Parameters"은 강력한 소프트웨어 테스팅 방법론인 “기호 실행(Symbolic Execution)”의 성능을 높이기 위해, 완전히 자동화된 외부 파라미터 값 조정(external parameter tuning) 기술을 제안한다. 학계나 산업계에서 널리 사용되는 실용적인 기호 실행 도구들은 일반적으로 그 성능에 영향을 끼치는 다양한 외부 파라미터들을 적게는 수십 개에서 많게는 수백 개까지 포함하고 있다. 그러나, 기호 실행을 기존의 파라미터 조정 기술들은 테스트 대상 소프트웨어마다 수작업으로 값을 조정하거나 사용자의 개입을 요구하는 반자동화(Semi-Automatic) 방식만 존재했다. 본 논문에서는 학계에 잘 알려진 두 가지 기호 실행 도구들(KLEE, CREST)에 사용자의 개입이 없이도 적절한 외부 파라미터 값을 자동으로 선정할 수 있는 방법인 ParaSuit를 제안한다. 실험적으로, ParaSuit는 다수의 오픈소스-C 프로그램을 대상으로 기존의 최신 파라미터 조정 기술과 비교해서 분기 커버리지(Branch Coverage)와 오류 검출 능력을 크게 향상시키는데 성공하였다.

[논문 정보]

-  제목: Enhancing Symbolic Execution with Self-Configuring Parameters

-  저자: 김민종, 차수영

-  학회: IEEE/ACM International Conference on Software Engineering (ICSE 2026)

Abstract:

We present ParaSuit, a self-configuring technique that enhances symbolic execution by autonomously adjusting its parameters tailored to each program under test. Modern symbolic execution tools are typically equipped with various external parameters to effectively test real-world programs. However, the need for users to fine-tune a multitude of parameters for optimal testing outcomes makes these tools harder to use and limits their potential benefits. Despite recent efforts to improve this tuning process, existing techniques are not self-configuring; they cannot dynamically identify which parameters to tune for each target program, and for each manually selected parameter, they sample a value from a fixed, user-defined set of candidate values that is specific to that parameter and remains unchanged across programs. The goal of this paper is to automatically configure symbolic execution parameters from scratch for each program. To this end, ParaSuit begins by automatically identifying all available parameters in the symbolic execution tool and evaluating each parameter’s impact through interactions with the tool. It then applies a specialized algorithm to iteratively select promising parameters, construct sampling spaces for each, and update their sampling probabilities based on data accumulated from symbolic execution runs using sampled parameter values. We implemented ParaSuit on KLEE and assessed it across 12 open-source C programs. The results demonstrate that ParaSuit significantly outperforms the state-of-the-art method without selfconfiguring parameters, achieving an average of 26% higher branch coverage. Remarkably, ParaSuit identified 11 unique bugs, four of which were exclusively discovered by ParaSuit.