Symetra : visual analytics for tuning symbolic execution engines

다국어 초록 (Multilingual Abstract)

In software testing, symbolic execution engines such as KLEE are widely used to automatically generate test cases, aiming to maximize the number of branches executed by the test cases, i.e., branch coverage. While branch coverage is heavily affected by the parameters provided to the engine, the multidimensional nature of these parameters complicates understanding their impact on branch coverage. As a result, the user often relies on default configurations, which leads to suboptimal results. In this work, we present a visual analytics system, Symetra, designed to support the parameter tuning process of symbolic execution engines. To handle a large number of parameters and their configurations, we provide two complementary overviews of their impact on branch coverage values and patterns. Building on these overviews, our system enables collective analysis where the user can compare two groups of configurations to analyze the differences that may cause differences in branch coverage. Through case studies and expert interviews, we demonstrate that the experts were able to not only understand the impact of parameters on branch coverage but also identify their complementary nature to improve branch coverage more efficiently. Furthermore, we showcase a use case of Human-in-the-Loop parameter tuning, where experts iteratively used our system to improve branch coverage and reduce the number of failed runs.

국문 초록 (Abstract)

소프트웨어 테스팅에서 KLEE와 같은 심볼릭 실행 엔진은 테스트 케이스를 자동으로 생성하는 데 널리 사용되며, 이를 통해 분기 커버리지를 극대화하는 것을 목표로 한다. 분기 커버리지는 엔진에 제공되는 파라미터의 영향을 크게 받지만, 파라미터의 다차원적 특성으로 인해 분기 커버리지에 미치는 영향을 이해하기 어렵다. 결과적으로 사용자는 기본 설정에 의존하게 되고, 이는 최적이 아닌 결과로 이어진다. 본 연구에서는 심볼릭 실행 엔진의 파라미터 튜닝 과정을 지원하기 위해 설계된 시각 분석 시스템인 Symetra를 제시한다. 다수의 파라미터와 설정을 처리하기 위해, 분기 커버리지 값과 패턴에 대한 두 가지 상호보완적인 개요를 제공한다. 이러한 개요를 바탕으로, 사용자는 두 설정 그룹을 비교하여 분기 커버리지의 차이를 유발할 수 있는 차이점을 분석하는 집합적 분석을 수행할 수 있다. 사례 연구와 전문가 인터뷰를 통해, 전문가들이 파라미터가 분기 커버리지에 미치는 영향을 이해할 뿐만 아니라 파라미터의 상호보완적 특성을 파악하여 분기 커버리지를 더 효율적으로 개선할 수 있었음을 확인하였다. 또한 전문가들이 시스템을 반복적으로 사용하여 분기 커버리지를 개선하고 실패한 실행 횟수를 줄인 Human-in-the-Loop 파라미터 튜닝 사례를 제시한다.

목차 (Table of Contents)

• Chapter 1. INTRODUCTION 1
• Chapter 2. RELATED WORK 4
• 1. Parameter Tuning for Symbolic Execution 4
• 2. Visual Analytics Systems for Parameter Tuning 5
• Chapter 3. DOMAIN ANALYSIS 8
• 1. Background and Terminology 8
• 2. User Goals and Tasks 11
• Chapter 4. THE Symetra SYSTEM 14
• 1. Design Goals 14
• 2. User Interface 16
• 3. Implementation 26
• Chapter 5. CASE STUDY 27
• 1. P1: Investigating Parameter Effects and Discovering 29
• Complementary Search Strategies
• 2. P2: Preventing Failed Runs and Optimizing Seed File 32
• Selection 32
• 3. Discussion 35
• 4. Expert Interviews 37
• Chapter 6. USE CASE: HUMAN-IN-THE-LOOP PARAMETER TUNING 39
• Chapter 7. LIMITATIONS AND FUTURE WORK 42
• Chapter 8. CONCLUSION 44
• References 45