Stephen F. Siegel

Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation

This paper presents an approach to use LLMs in a limited setting to generate a small, human-certifiable ACSL contract from the function's documentation, combined with a deterministic toolchain that supports a restricted ACSL profile and generates a driver that uses the CIVL verifier to check the implementation against...