lh-l4v

History

Gerwin Klein 0d984f3fa3 camkes: update to Isabelle2023 mapsto syntax Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>		2023-10-06 14:41:53 +11:00
..
adl-spec	Fix refs_valid_procedures definition	2021-03-24 10:47:01 +11:00
cdl-refine	camkes: update to Isabelle2023 mapsto syntax	2023-10-06 14:41:53 +11:00
glue-proofs	license: provide documentation under CC-BY-SA-4.0	2020-03-16 14:19:15 +08:00
glue-spec	all: remove theory import path references	2020-11-02 10:16:17 +10:00
Makefile	Makefiles: remove unused report-regression target	2022-06-03 09:36:43 +10:00
README	licenses: convert license tags to SPDX	2020-03-13 14:38:24 +08:00
ROOT	camkes: ROOT updates	2020-10-27 15:52:31 +10:00
tests.xml	licenses: convert license tags to SPDX	2020-03-13 14:38:24 +08:00

README

<!--
     Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)

     SPDX-License-Identifier: GPL-2.0-only
-->

CAmkES is a component platform for seL4. This directory contains files related
to a formal Isabelle model of CAmkES.

 adl-spec/ - Architectural model.
 glue-proofs/ - AutoCorres-based work (bottom-up approach to glue code).
 glue-spec/ - Behavioural model (top-down approach to glue code).