adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
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
..
access-control proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
asmrefine isabelle2021-1: remove no_take_bit 2022-03-29 08:38:25 +11:00
bisim proof+autocorres: update for select_wp and alternative_wp 2023-08-09 16:42:01 +10:00
capDL-api capdDL-api: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:53 +11:00
crefine 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
dpolicy various: resolve some new fixmes 2021-11-12 09:39:16 +11:00
drefine 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
infoflow 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
invariant-abstract 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
refine lib: reorder assumptions of no_fail_bind 2024-01-15 18:08:12 +10:30
sep-capDL sep-capDL: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:53 +11:00
Makefile proof: switch AArch64 quick_and_dirty from Refine to CRefine 2023-10-13 09:12:09 +11:00
README.md license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
ROOT proof/ROOT: RefineOrphanage: add quick and dirty option 2023-05-26 18:04:49 +10:00
tests.xml regression: increase CRefine timeout 2020-11-26 00:31:04 +11:00

README.md

Formal Proofs about seL4

This directory contains the formal proofs about seL4, which mostly prove properties about the various seL4 specifications.

Each such proof lives in its own subdirectory: