adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/spec
History
Rafal Kolanski ea771a8f7c arm-hyp: configure kernel Makefile for L4V_ARCH=ARM_HYP 
Set as required for TK1 platform.
 		2017-03-06 17:16:28 +11:00
..
abstract aspec: standard file access rights 2017-03-04 10:32:12 +11:00
capDL capDL spec and DRefine: updates for Hypervisor stub 2017-02-22 15:26:50 +11:00
cspec arm-hyp: configure kernel Makefile for L4V_ARCH=ARM_HYP 2017-03-06 17:16:28 +11:00
design licenses: Updated licenses added from x64 backport 2017-02-28 12:26:19 +11:00
haskell haskell: add Hypervisor module, add concept of Hypervisor exceptions 2017-02-22 15:26:41 +11:00
machine execspec: add hypervisor, HypFaultType in skeletons (ARM), generated files 2017-02-22 15:26:46 +11: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 cspec: build: avoid re-entering isabelle via dash-0.5.8 2016-02-17 11:04:20 +11:00
README.md misc: Proofing and formatting of README.md files. 2014-07-28 13:15:48 +10:00
ROOT backport changes to ARM proofs from X64 work in progress 2017-01-27 08:31:07 +11:00
tests.xml regression: add test for building Haskell kernel 2016-05-24 14:52:51 +10:00

README.md

Formal Specifications of seL4

See the sub directories for more details.

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