e2e-case-study

Dependencies

C parser document

Raw isabelle

C parser - Chose the newest version here. (Java also required here)

In order to put the parser up, the version of Isabelle and MLton matters, which can be found here

Possible errors when building MLton

seL4 on Docker

When trying to build docker with M1 system, might run into an error, this can be fixed by editing docker engine configuration and disable buildkit

Tutorial setup

$ mkdir tutorial
$ cd tutorial
$ repo init -u https://github.com/seL4/sel4-tutorials-manifest.git

Setting the proof up:

1. Follow the instructions to setup isabelle
2. Run proof following the description