History

Alejandro Gomez-Londono 4a76aec383 arm-hyp test: Fix race condition between ARM tests		2017-06-19 14:32:24 +10:00
..
abstract	arm-hyp abtract: update the sanitise_register definition (rebasing done)	2017-06-19 14:32:24 +10:00
capDL	capDL spec and DRefine: updates for Hypervisor stub	2017-02-22 15:26:50 +11:00
cspec	cspec/crefine: readme: document significance of L4V_ARCH	2017-03-31 16:13:42 +11:00
design	arm-hyp abstract/design: add VCPU banked register machine ops	2017-06-19 14:32:24 +10:00
haskell	arm-hyp haskell: add banked register machine ops	2017-06-19 14:32:24 +10:00
machine	arm-hyp design/abstract: clean up and indent MachineOps	2017-06-19 14:32:24 +10:00
sep-abstract	Bisim / Access / InfoFlow: updates for Hypervisor stub	2017-02-22 15:26:49 +11:00
take-grant	Isabelle2016-1: fix proofs involving UNION	2017-01-05 14:27:33 +11:00
Makefile	Remove spec-check test and scripts	2017-05-12 12:50:55 +10:00
README.md	misc: Proofing and formatting of README.md files.	2014-07-28 13:15:48 +10:00
ROOT	cspec: move to ARM subdirectory	2017-03-30 18:20:24 +11:00
tests.xml	arm-hyp test: Fix race condition between ARM tests	2017-06-19 14:32:24 +10:00

Formal Specifications of seL4

See the sub directories for more details.

The Makefile and ROOT file define runnable Isabelle sessions for these specifications.