adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Santiago Bautista ab259704c7 access+infoflow+drefine: update for new definition of `idle_tcb_at` 
* Context :

 We would like to prove that, for ARM_HYP architecture,
  the current vcpu is always the vcpu associated to the current thread.
 See issue https://jira.csiro.au/browse/VER-770
  and PR 291 http://bitbucket.keg.ertos.in.nicta.com.au/projects/SEL4/repos/l4v/pull-requests/291

 In this process, we changed the definition of `idle_tcb_at`

* In this commit :

 Update some proofs in access, infoflow and drefine to take
  the new definition of `idle_tcb_at` into account.
 		2018-10-31 18:04:59 +11:00
..
access-control access+infoflow+drefine: update for new definition of `idle_tcb_at` 2018-10-31 18:04:59 +11:00
asmrefine Isabelle2018: new AsmRefine session + test 2018-08-20 09:06:36 +10:00
bisim Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
capDL-api Base ASpec + machine on OptionMonad_ND; fix proof fallout 2018-10-25 12:54:02 +11:00
crefine crefine: arm-hyp: add word lemma FIXMEs 2018-10-10 14:15:01 +11:00
drefine access+infoflow+drefine: update for new definition of `idle_tcb_at` 2018-10-31 18:04:59 +11:00
infoflow access+infoflow+drefine: update for new definition of `idle_tcb_at` 2018-10-31 18:04:59 +11:00
invariant-abstract arm-hyp ainvs: prove that the vcpu of the idle thread is always None 2018-10-31 18:04:59 +11:00
refine Base ASpec + machine on OptionMonad_ND; fix proof fallout 2018-10-25 12:54:02 +11:00
sep-capDL lib+sysinit: add extended separation algebra and forward reasoning tactics 2018-09-18 12:01:52 +10:00
Makefile refine: move Orphanage to separate session, RefineOrphanage 2018-10-03 19:47:04 +10:00
README.md integrate separation kernel config proofs 2014-08-13 22:08:46 +10:00
ROOT reduce DRefine dependencies from Refine to AInvs 2018-10-22 13:21:11 +11:00
tests.xml test: allow CBaseRefine to run concurrently with Refine 2018-10-22 13:21:11 +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: