AutoCorres 1.11 and C-Parser 1.21

AutoCorres 1.11

• Isabelle2024 edition of AutoCorres
• Further clean-up and restructure of monad libraries.

C Parser 1.21

• Isabelle2024 edition of the C Parser
• Updated SIMPL from the AFP
• Ensure that umm_types.txt is saved relative to theory file
• If cpp_path is relative, make it relative to the current theory

Proofs for seL4 13.0.0

Proof compatible with seL4 release 13.0.0.

AutoCorres 1.10 and C-Parser 1.20

AutoCorres 1.10

• Isabelle2023 edition of AutoCorres
• Restructured and cleaned up monad libraries. Removed dependencies on unrelated l4v libraries.

C Parser 1.20

• Isabelle2023 edition of the C Parser
• Rearranged library session structure and included more libraries for heap reasoning in the release. See e.g. files TypHeapLib.thy and LemmaBucket_C.thy

AutoCorres 1.9 and C-Parser 1.19

AutoCorres 1.9 (31 October 2022)

• Isabelle2021-1 edition of both AutoCorres and the C parser.
• setup for AARCH64/ARM64 targets

C-Parser 1.19

• Builds with Isabelle2021-1

• setup for AARCH64/ARM64 targets

• AST printing for top-level declarations annotated to make them easier to
  consume in external tools. Annotations take the form:

  ##<decl_type>: <name>
  

  e.g. ##Function: ctzl

Autocorres 1.8 and CParser 1.18

AutoCorres 1.8 (31 October 2021)

• Isabelle2021 edition of both AutoCorres and the C parser.

CParser 1.18

• Builds with Isabelle2021
• improve inline assembly support in modifies proofs
• always use fresh names for generated temporary variables.
  This fixes a problem that could make some function call expressions unprovable. (VER-1389)
• improve compile time performance for functional record update definitions

Proofs for seL4 12.1.0

Version compatible with seL4 12.1.0

Proofs for seL4-12.0.0

Version compatible with seL4 12.0.0

Proofs for seL4-11.0.0

Version compatible with seL4 11.0.0

Proofs for seL4-8.0.0

Isabelle/HOL proofs seL4-8.0.0

Proofs for seL4-7.0.0

Isabelle/HOL proofs for seL4-7.0.0