Numerical Methods in Isabelle

Formalisation and verification of several numerical algorithms in the Isabelle/ITree framework. Extended comparison with the refinement framework and initial attempts to account for floating-point implementations of the algorithms. Assembling the artefact from its split parts============================================ This Zenodo record hosts the artefact as a split ZIP archive. The archive is~1.4 GB because the bundled, ready-to-run Docker image contains the prebuiltIsabelle2025/UTP heap images, so it is uploaded as ten ~150 MiB parts. Rebuildthe single archive as follows. 1. Download all files named sefm_artefact.zip.part-aa ... sefm_artefact.zip.part-aj together with PARTS.sha256 into one directory. 2. (Optional) Verify each downloaded part is intact: shasum -a 256 -c PARTS.sha256 # macOS sha256sum -c PARTS.sha256 # Linux Every part must report OK. 3. Reassemble the ZIP. The shell glob restores the correct aa, ab, ... order: cat sefm_artefact.zip.part-* > sefm_artefact.zip The reassembled archive must have this SHA-256: d8ca17cea33234037d246372065a2b68991591fdfa3dca109c4d0e32d86eb50b sefm_artefact.zip Check it with: shasum -a 256 sefm_artefact.zip # macOS sha256sum sefm_artefact.zip # Linux 4. Unzip and verify the full payload against the shipped manifest: unzip sefm_artefact.zip cd sefm_artefact shasum -a 256 -c MANIFEST.sha256 # macOS sha256sum -c MANIFEST.sha256 # Linux All six payload files must report OK. 5. Follow README.md inside the extracted sefm_artefact/ directory for the quick start, functional evaluation, and reusability evaluation.