Automated Verification with LLMs for Large Programs

This paper addresses the challenge of verifying large-scale software by combining static analysis, deductive verification, and LLMs. It introduces Preguss, a framework that uses LLMs to generate and refine formal specifications, guided by potential runtime errors. The key contribution is the modular, fine-grained approach that allows for verification of programs with over a thousand lines of code, significantly reducing human effort compared to existing LLM-based methods.