adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/spec
History
Daniel Matichuk 0063075ba4 Merge remote-tracking branch 'verification/master' into arch_split 2016-01-28 18:26:53 +11:00
..
abstract Merge remote-tracking branch 'verification/master' into arch_split 2016-01-21 10:22:48 +11:00
capDL arch_split: DRefine now builds 2016-01-25 18:42:27 +11:00
cspec Merge remote-tracking branch 'verification/master' into arch_split 2016-01-28 18:26:53 +11:00
design Merge remote-tracking branch 'verification/master' into arch_split 2016-01-21 10:22:48 +11:00
machine paramatrised abstract and haskell specs over L4V_ARCH 2016-01-13 12:01:40 +11:00
sep-abstract terminology in comments: async ep -> notifications 2015-11-24 16:58:22 +13:00
take-grant remove syntax ambiguity 2015-05-09 13:04:11 +02:00
Makefile paramatrised abstract and haskell specs over L4V_ARCH 2016-01-13 12:01:40 +11:00
README.md misc: Proofing and formatting of README.md files. 2014-07-28 13:15:48 +10:00
ROOT paramatrised abstract and haskell specs over L4V_ARCH 2016-01-13 12:01:40 +11:00
tests.xml regression: fix tests.xml dependencies to be consistent with ROOTs. 2016-01-07 18:39:50 +11: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.