VeRefine : A Workflow for the Generation, Formal Verification, and Evaluation of Function Contracts in ANSI/ISO C Specification Language (ACSL)

Sammanfattning

This thesis presents VeRefine, a novel workflow motivated by the limited adoption of formal verification in the automotive industry. VeRefine combines Artificial Intelligence (AI) with formal methods by employing a Large Language Model (LLM) to automatically generate formal specifications in ANSI/ISO C Specification Language (ACSL), restricted to preconditions and postconditions, the Framework for Modular Analysis of C programs (FramaC) as the tool for formal verification of C functions, and a formal evaluation process based on contract refinement to compare AI-generated formal specifications with trusted human-written ones. The workflow was tested on a dataset of 45 C functions, achieving a 100% success rate in producing formal specifications. However, only 33.3% of the AI-generated formal specifications were equal to or stronger than their human-written counterparts, with one case where the AI output refined the expert’s formal specification. These findings indicate that while LLMs can meaningfully assist in formal specification generation and contribute to formal verification workflows, significant limitations remain that need to be addressed in future research.