Experiments and other Supplementary Data

In the following we give some experimental results and further supplementary data for different papers and different versions of IsaFoR and CeTA.

• IsaFoR Version 3.8
  We used this version to generate supplementary data for the paper New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations (FSCD'26).
• AFP 2025-1
  We used this version to generate supplementary data for the paper A verified algorithm for deciding pattern completeness with optimal asymptotic complexity (JLAMP in 2026).
• IsaFoR/CeTA Version 3.3
  We used this version to generate supplementary data for the paper An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting (CPP'25).
• AFP 2024
  We used this version to generate supplementary data for the paper A verified algorithm for deciding pattern completeness (FSCD'24).
• IsaFoR/CeTA Version 2.46
  We used this version to generate supplementary data for the paper Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs (CPP'24).
• IsaFoR/CeTA Version 2.??
  We used this version to generate supplementary data for the paper An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR (CPP'21).
• IsaFoR/CeTA Version 2.39
  We tested this version of CeTA for the paper Certifying the Weighted Path Order (FSCD'20). The results within the paper have been obtained in combination with NaTT and TTT2.
• IsaFoR/CeTA Version 2.38
  We tested this version of CeTA for the paper Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL (NFM'20). The results within the paper have been obtained in combination with Z3 and CVC4.
• experimental data of papers earlier than 2019 is no longer available because of a change of servers; if you urgently require this data, please contact René Thiemann directly