Toward improving symbolic execution : empirical lessons from human-written test cases

다국어 초록 (Multilingual Abstract)

Symbolic execution has long been a cornerstone of automated test generation, yet it continues to grapple with fundamental challenges such as path explosion and constraint-solving overhead. Decades of research have introduced advanced techniques---including search heuristics, state pruning, and constraint-solving optimizations---but whether they outperform human test writers in practice remains unclear. We present a large-scale empirical study comparing human-written and symbolic execution–generated test cases across six real-world C programs. One hundred undergraduate students manually wrote 3,000 test cases per program, resulting in a total of 18,000 test cases, which we compared against those produced by four state-of-the-art symbolic execution techniques. Surprisingly, the human-written tests achieved up to 2.6× higher branch coverage, even though they were outnumbered 30 to 1. To understand this gap, we conducted a comparative analysis across three dimensions: surface-level input features, code coverage differences, and program-state complexity. Our results show that human inputs tend to be longer, more complex, and better suited to triggering behavior in challenging code regions---especially those involving regular expressions and switch statements. Finally, we explored simple human-inspired modifications to symbolic execution, including argument shaping, regular expression injection, and test case seeding. While these yielded mixed results, they exposed promising and underexplored directions for improving symbolic execution effectiveness.

국문 초록 (Abstract)

기호실행은 오래전부터 자동 테스트 생성의 핵심 기법이었지만, 경로 폭발과 제약 해결 오버헤드 같은 근본적 문제로 여전히 어려움을 겪고 있다. 수십년 간의 연구는 검색 휴리스틱, 상태 가지치기, 제약 해결 최적화 등 다양한 고급 기법을 제시해 왔으나, 실제로 이러한 기법이 인간 테스트 작성자를 능가하는지는 명확하지 않다. 본 연구는 여섯 개의 실 세계 C 프로그램을 대상으로 인간이 작성한 테스트 케이스와 기호실행으로 생성된 테스트 케이스를 대규모로 비교한 실증 연구를 제시한다. 100명의 학부생이 프로그램당 3,000개의 테스트를 수동으로 작성하여 총 18,000개의 테스트 케이스를 만들었고, 이를 최신 기호실행 기법 네 가지가 생성한 테스트와 비교하였다. 놀랍게도, 인간이 작성한 테스트는 수적으로 30:1로 열세였음에도 최대 2.6배 더 높은 분기 커버리지를 달성했다. 이 격차를 이해하기 위해 우리는 (1) 표면적 입력 특성, (2) 코드 커버리지 차이, (3) 프로그램 상태 복잡도라는 세 가지 차원에서 비교 분석을 수행했다. 그 결과, 인간 입력은 더 길고 복잡하며, 특히 정규 표현식과 switch 문이 관여하는 도전적인 코드 영역의 동작을 유발하는 데 더 적합한 경향이 있음을 확인했다. 마지막으로, 우리는 인자 형태 조정(argument shaping), 정규 표현식 주입, 테스트 케이스 시딩 등 인간에게서 영감을 얻은 단순한 수정들을 기호실행에 적용해 보았다. 결과는 엇갈렸지만, 이러한 시도는 기호실행의 효과성을 높이기 위한 유망하면서도 아직 충분히 탐구되지 않은 방향을 드러냈다.

목차 (Table of Contents)

• Chapter 1. Introduction 1
• 1. Contributions 3
• Chapter 2. Preliminaries 5
• 1. Symbolic Execution 5
• 2. Diverse Techniques for Symbolic Execution 6
• 3. Motivation 7
• Chapter 3. Research Questions 10
• 1. Research Questions 10
• 2. Subject Programs 10
• 3. Manual Test Case Generation 11
• 4. Automated Symbolic Execution Setup 14
• Chapter 4. Comprehensive Empirical Research 16
• 1. RQ1: What are the surface-level differences between symbolic execution-generated and human-generated test cases 16
• 2. RQ2: Which code regions are covered exclusively by manually generated test cases 20
• 3. RQ3: What are the program state-level differences between inputs generated by symbolic execution and those generated by humans 26
• 4. Direction of Future Research 30
• 5. Threats to Validity 31
• Chapter 5. Related Works 33
• 1. Boosting Symbolic Execution 33
• 2. Empirical Research on Symbolic Execution 34
• Chapter 6. Conclusion 35
• References 36
• Korean Abstract 39