Formal verification provides a rigorous and systematic approach to ensuring the correctness and reliability of software systems. Yet, constructing specifications for the complete proof relies on domain expertise and non-trivial manpower. In view of such needs, an automated specification synthesis approach is desired. Existing automated specification synthesis approaches are limited in versatility, i.e.,  they either focus only on synthesizing loop invariants for numerical programs, or are tailored for specific types of programs or invariants. While the programs mix with more complicated data types (e.g., arrays, pointers) and code structures (e.g., nested loop, function calls) are beyond their capability. Given this research gap, we present an automated specification synthesis approach, AutoSpec, for automated program verification. It overcomes the shortcomings of existing work in specification versatility, synthesizing satisfiable and adequate specifications for complete proof. It is driven by static analysis and program verification, and is empowered by large language models (LLMs). AutoSpec addresses the practical challenges three-fold: (1) driving AutoSpec by static analysis and program verification, LLMs serve as candidate specification generators, (2) decomposing the programs to lead LLMs' attention, and (3) validating the candidate specifications at each round to avoid error accumulation during LLM's interaction. By doing so, AutoSpec can incrementally and iteratively generate satisfiable and adequate specifications. The evaluation shows its effectiveness and usefulness. AutoSpec can handle 79% of them, 1.592X outperforming existing works. It can also be successfully applied to verify the programs in a real-world X509-parser project. 

We have released the implementation and all associated publicly available data to encourage comparable and evidence-based studies on specification Generation for deductive verification. 

Package Download: https://zenodo.org/doi/10.5281/zenodo.10912657

The package includes (1) four benchmarks, containing 251 C programs and 100 mutated programs, each with specific properties to be verified. (2) the annotated version of 251 C programs filled with specifications that are strong enough to verify the desired properties. (3) An available tool \name implements a pipeline for specification generation and automatic verification. It takes the source code of a C program as input and outputs the verification result, along with an annotated version filled with specifications. (4) Some raw experimental data.

# 1. Directory Structure