Search papers, labs, and topics across Lattice.
This paper explores using LLMs to generate counterexamples for invalid assertions inferred by dynamic analysis tools like SpecFuzzer, addressing the issue of over-generalized assertions due to incomplete test suites. By leveraging LLMs to create tests that attempt to invalidate candidate assertions, the approach effectively filters out false positives. Experiments show that LLM-generated counterexamples can discard up to 11.68% of invalid assertions and improve the precision of inferred specifications by up to 7% without impacting recall.
LLMs can slash false positives in dynamic specification inference by generating targeted counterexamples, boosting assertion precision by up to 7%.
Contract assertions, such as preconditions, postconditions, and invariants, play a crucial role in software development, enabling applications such as program verification, test generation, and debugging. Despite their benefits, the adoption of contract assertions is limited, due to the difficulty of manually producing such assertions. Dynamic analysis-based approaches, such as Daikon, can aid in this task by inferring expressive assertions from execution traces. However, a fundamental weakness of these methods is their reliance on the thoroughness of the test suites used for dynamic analysis. When these test suites do not contain sufficiently diverse tests, the inferred assertions are often not generalizable, leading to a high rate of invalid candidates (false positives) that must be manually filtered out. In this paper, we explore the use of large language models (LLMs) to automatically generate tests that attempt to invalidate generated assertions. Our results show that state-of-the-art LLMs can generate effective counterexamples that help to discard up to 11.68\% of invalid assertions inferred by SpecFuzzer. Moreover, when incorporating these LLM-generated counterexamples into the dynamic analysis process, we observe an improvement of up to 7\% in precision of the inferred specifications, with respect to the ground-truths gathered from the evaluation benchmarks, without affecting recall.
