CFStra: Enhancing Configurable Program Analysis Through LLM-Driven Strategy Selection Based on Code Features

Configurable Program Analysis (CPA) allows users to customize program analysis based on their preferences. However, current program verification tools like Cpachecker require manual strategy selection, which can be complex and error-prone. In this paper, we present a novel approach to efficiently perform program verification tasks by harnessing the capabilities of Large Language Models (LLMs) to automatically select verification strategies based on code features and specifications. Specifically, we begin by extracting relevant code snippets and querying LLMs to identify code features. Based on the identified code features, we propose a strategy selector to automatically choose the verification strategy. Finally, we execute the Cpachecker with the selected verification strategy. We evaluated our approach using a diverse set of 600 verification tasks. The results demonstrate the effectiveness of our approach, surpassing basic strategies and SOTA combination strategies while also standing out for its simplicity and ease of understanding.