README.md
1CapDL API Proofs
2================
3
4This proof develops a formal API description for a number of the seL4
5system calls, of the [capDL](../../spec/capDL/) kernel specification.
6This API description is a set of lemmas describing the behaviour of
7various system calls in terms of a [separation logic](../sep-capDL/)
8defined over that kernel specification.
9
10When reasoning about system calls this proof treats the kernel like
11a library invoked directly from user-space and does not reason about
12scheduling. These proofs are used by the [system initialiser
13proof](../../sys-init), as described in the [ICFEM '13 paper][Boyton_13]
14and Andrew Boyton's PhD thesis.
15
16 [Boyton_13]: http://www.nicta.com.au/pub?id=7047 "Formally Verified System Initialisation"
17
18Building
19--------
20
21To build from the `l4v/` directory, run:
22
23 ./isabelle/bin/isabelle build -d . -v -b DSpecProofs
24
25Important Theories
26------------------
27
28The top-level theory is [`API_DP`](API_DP.thy). The seL4 API and kernel
29model are located in [`Kernel_DP`](Kernel_DP.thy).
30
31