Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
arxiv(2024)
摘要
Formal verification provides a rigorous and systematic approach to ensure the
correctness and reliability of software systems. Yet, constructing
specifications for the full proof relies on domain expertise and non-trivial
manpower. In view of such needs, an automated approach for specification
synthesis is desired. While existing automated approaches are limited in their
versatility, i.e., they either focus only on synthesizing loop invariants for
numerical programs, or are tailored for specific types of programs or
invariants. Programs involving multiple complicated data types (e.g., arrays,
pointers) and code structures (e.g., nested loops, function calls) are often
beyond their capabilities. To help bridge this gap, we present AutoSpec, an
automated approach to synthesize specifications for automated program
verification. It overcomes the shortcomings of existing work in specification
versatility, synthesizing satisfiable and adequate specifications for full
proof. It is driven by static analysis and program verification, and is
empowered by large language models (LLMs). AutoSpec addresses the practical
challenges in three ways: (1) driving by static analysis and program
verification, LLMs serve as generators to generate candidate specifications,
(2) programs are decomposed to direct the attention of LLMs, and (3) candidate
specifications are validated in each round to avoid error accumulation during
the interaction with LLMs. In this way, AutoSpec can incrementally and
iteratively generate satisfiable and adequate specifications. The evaluation
shows its effectiveness and usefulness, as it outperforms existing works by
successfully verifying 79
synthesis, a significant improvement of 1.592x. It can also be successfully
applied to verify the programs in a real-world X509-parser project.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要