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

arXiv:2609.31687v1 Announce Type: new Abstract: Parallel numerical libraries such as PETSc are widely used in science and engineering applications where wrong results can have costly consequences. Despite this,...