Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation
Parallel numerical libraries such as PETSc are widely used in science and engineering applications where wrong results can have costly consequences. Despite this, numerical libraries are rarely formally verified. One of the challenges is the need for an expert to hand-write a specification and manually apply a verification tool, often requiring the development of a harness or driver, all of which can contain additional bugs that lead to false positives or false negatives during verification. With recent advancements in large language models (LLMs), it is tempting to generate such drivers and reference models automatically, but one-shot generation based on a simple prompt is brittle and le...
| Authors | Hansol Suh, Jan Hückelheim, Stephen Siegel |
|---|---|
| Primary category | cs.CL |
| Published | 16 September 2026 |
| Last updated at source | 16 September 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 17 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.