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

Hansol Suh, Jan Hückelheim, Stephen Siegel

Parallel numerical libraries such as PETSc are widely used in science and engineering applications where wrong results can have costly consequences. Despite this, numerical librari…