Scholarlink

<p>Symbolic execution is a powerful technique for automated test case generation, ensuring comprehensive coverage of potential scenarios. However, it often struggles with complex, deep paths due to path explosion. Conversely, large language models (LLMs) utilize vast training data to generate test cases that can uncover intricate program behaviors that symbolic execution might miss. Despite their complementary strengths, integrating the systematic nature of symbolic execution with the creative capabilities of LLMs presents a significant challenge. We introduce <span>NexuSym</span>, an innovative tool that integrates symbolic execution with LLMs to facilitate the automatic generation of test cases. To effectively bridge the gap between these two approaches, we have developed a test case reducer, which normalizes the LLM-generated test cases to make them compatible with symbolic execution. Additionally, we propose a search space summarizer, which abstracts and condenses the search space explored by symbolic execution, enabling the LLM to focus on the most promising areas for further exploration. We instantiated <span>NexuSym</span> on KLEE and ChatGPT. Our evaluation of <span>NexuSym</span> involved 99 coreutils programs and 9 large GNU programs. The experimental results demonstrate that <span>NexuSym</span> significantly enhances program test coverage, with improvements of up to 20% in certain cases. Furthermore, we conducted an analysis of the monetary costs associated with using the LLM API, revealing that <span>NexuSym</span> is a highly cost-effective solution.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

NexuSym: Marrying symbolic path finders with large language models

  • 期刊论文

  • 发表日期：

    2025年6月7日

查看全文
  • Jiayi Wang,
  • Ping Yu,
  • Yi Qin,
  • Yanyan Jiang,
  • Yuan Yao,
  • Xiaoxing Ma

摘要

Symbolic execution is a powerful technique for automated test case generation, ensuring comprehensive coverage of potential scenarios. However, it often struggles with complex, deep paths due to path explosion. Conversely, large language models (LLMs) utilize vast training data to generate test cases that can uncover intricate program behaviors that symbolic execution might miss. Despite their complementary strengths, integrating the systematic nature of symbolic execution with the creative capabilities of LLMs presents a significant challenge. We introduce NexuSym, an innovative tool that integrates symbolic execution with LLMs to facilitate the automatic generation of test cases. To effectively bridge the gap between these two approaches, we have developed a test case reducer, which normalizes the LLM-generated test cases to make them compatible with symbolic execution. Additionally, we propose a search space summarizer, which abstracts and condenses the search space explored by symbolic execution, enabling the LLM to focus on the most promising areas for further exploration. We instantiated NexuSym on KLEE and ChatGPT. Our evaluation of NexuSym involved 99 coreutils programs and 9 large GNU programs. The experimental results demonstrate that NexuSym significantly enhances program test coverage, with improvements of up to 20% in certain cases. Furthermore, we conducted an analysis of the monetary costs associated with using the LLM API, revealing that NexuSym is a highly cost-effective solution.