NameDateSize

..25-Jul-201916

API_DP.thyH A D25-Jul-2019317

Arch_DP.thyH A D25-Jul-201933.1 KiB

CNode_DP.thyH A D25-Jul-201934.6 KiB

Invocation_DP.thyH A D25-Jul-201954.8 KiB

IRQ_DP.thyH A D25-Jul-201921.9 KiB

Kernel_DP.thyH A D25-Jul-201912.3 KiB

KHeap_DP.thyH A D25-Jul-201949.3 KiB

ProofHelpers_DP.thyH A D25-Jul-20192.3 KiB

README.mdH A D25-Jul-20191 KiB

Retype_DP.thyH A D25-Jul-201954 KiB

RWHelper_DP.thyH A D25-Jul-201920.7 KiB

Sep_Tactic_Examples.thyH A D25-Jul-201910.1 KiB

TCB_DP.thyH A D25-Jul-201963.8 KiB

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