adbrucker/lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
master
lh-l4v/spec
History
Achim D. Brucker e59d6ad091 Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name.
2024-01-27 13:44:24 +00:00
..
abstract aarch64 machine+aspec+cspec: pt_type ghost+table array sizes 2024-01-16 10:01:47 +11:00
capDL Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
cspec Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
design Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
haskell aarch64 haskell: check cap type in checkVSpaceRoot 2023-09-27 14:28:32 +10:00
machine Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
sep-abstract READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00
take-grant Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
Makefile Makefiles: remove unused report-regression target 2022-06-03 09:36:43 +10:00
README.md license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
ROOT Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
tests.xml haskell: constrain run_tests to current L4V_ARCH 2023-05-31 14:46:35 +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.