secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
seL4-L4.verified/spec
History
Gerwin Klein be238597cc arm+arm-hyp+aarch64 machine: fix GICv3 gicNumTargets_bits 
The value of gicNumTargets_bits was wrong for GICv3 platforms, breaking
CRefine for those platforms.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
 		2025-07-07 19:19:20 +10:00
..
abstract aspec+machine: SGISignalCap API + cdt interfaces 2025-07-07 08:53:07 +10:00
capDL capDL: add SGISignalCap API to capDL 2025-07-07 08:53:07 +10:00
cspec cspec: fix invalid escape sequence in mk_umm_types 2025-03-13 13:45:29 +11:00
design design+haskell-translator: SGI arch interfaces and caseconvs 2025-07-07 08:53:07 +10:00
haskell haskell: add SGISignalCap API 2025-07-07 08:53:07 +10:00
machine arm+arm-hyp+aarch64 machine: fix GICv3 gicNumTargets_bits 2025-07-07 19:19:20 +10:00
sep-abstract arm proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
take-grant READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11: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 isabelle2021-1: DSpec 2022-03-29 08:38:25 +11:00
tests.xml tests: make haskell-translator depend on kernel-config 2025-06-24 15:27:31 +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.