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.
arXiv - cs.CL (NLP)2 min read