e0b6d45db4
arm-hyp test: add BaseRefine to regression, set up REFINE_QUICK_AND_DIRETY for Refine
2017-06-19 14:32:23 +10:00
2ae9147f02
arm-hyp test: default targets for arm-hyp, turn on quick_and_dirty for AInvs
2017-06-19 14:32:20 +10:00
c41c7a97ca
update references from/to moved crefine, parametrise over L4V_ARCH
2017-03-31 16:13:41 +11:00
6ce6c97397
arch_split: DetSchedDomainTime_AI, DetSchedSchedule_AI for ARM
2017-03-09 12:10:44 +11:00
7657681fca
move refine/* to refine/ARM/*, parametrise over $L4V_ARCH
2017-01-30 12:22:22 +11:00
eb5badce92
l4v: Add intermediate image for InfoFlowC.
...
This allows one to skip the Access, InfoFlow proofs
when building InfoFlowC, hopefully allowing faster
turn arounds when doing maintenance.
2016-11-16 09:12:18 +11:00
d765a64b81
SELFOUR-444: Haskell implementation, begin refine.
...
First attempt at a haskell implementation of preemptible retyping
and the refinement proof to abstract.
2016-11-02 11:19:08 +11:00
445efb7c29
lib: closure for Word_Lib and own session
2016-05-16 21:11:40 +10:00
3144c4d847
Remove time limits from Isabelle ROOT files.
2016-02-29 14:52:37 +11:00
ca4391881c
WIP on WCET annotations.
2015-07-14 14:23:29 +10:00
f9e40c29db
cleanup: there already is a separate Bisim session
2015-04-19 10:24:42 +01:00
a221a52350
Added new proofcount tool to "tools" and removed old one from "lib".
...
Removed reference to old proof_counting from proof/ROOT and spec/ROOT
2015-02-11 17:46:34 +11:00
77c600038f
infoflow: fixed and added Example_Valid_StateH to testing
...
Some of the noninterference results depend on executions at the haskell level starting at a valid initial state. This file demonstrates this condition being realised.
2014-11-18 17:39:17 +11:00
f59767cdac
Slight fudges for Fastpath use with PIDE.
2014-09-18 20:12:43 +10:00
41c0e994ad
Make SIMPL->Graph regression testable.
2014-09-05 19:10:03 +10:00
f1d808c96a
integrate separation kernel config proofs
...
Hooked up into build system and regression test; added READMEs
2014-08-13 22:08:46 +10:00
c060f715db
Add a top-level file for the capDL API proofs.
2014-07-24 19:56:24 +10:00
2a03e81df4
Import release snapshot.
2014-07-14 21:32:44 +02:00
Miki Tanaka
Rafal Kolanski
Matthew Brecknell
Joel Beeren
Thomas Sewell
Gerwin Klein
Japheth Lim
Daniel Matichuk
deang
Andrew Boyton