Evaluating the Ability of OpenAI's GPT Large Language Models to Generate Verifiable Specifications in VeriFast for Heap-Manipulating C Code

While promising for automating the laborious task of writing specifications for static verification tools, OpenAI's GPT models, even with advanced prompting techniques, still struggle to consistently generate fully correct and verifiable specifications in VeriFast for heap-manipulating C code.