d1482e4ffa
misc: added skip proofs option for Refine
...
tags: [NO_PROOF]
2017-08-08 12:19:43 +10:00
796887d9b1
Removes all trailing whitespaces
2017-07-12 15:13:51 +10:00
9f32001c78
arm-hyp: enable quick_and_dirty for snd CBaseRefine image
2017-06-19 14:32:35 +10:00
96c13859e0
proof/ROOT: add CREFINE_QUICK_AND_DIRTY flag
...
Use to build CRefine in quick_and_dirty mode.
2017-06-19 14:32:35 +10:00
682dde4155
refine: add intermediate BaseRefine2 session for small machines
2017-06-19 14:32:29 +10:00
09a02acc7b
arm-hyp proofs/ROOT: make it possible to skip proofs in BaseRefine
2017-06-19 14:32:28 +10:00
740d606774
refine: closed the Orphanage
...
Not necessary for CRefine and better proved on the abstract spec now.
To be resurrected (on abstract) in the future.
2017-06-19 14:32:27 +10:00
3d22990928
arm-hyp test: setup REFINE_QUICK_AND_DIRTY for Refine (to be squashed)
...
* fix the order of entries in the ROOT file
2017-06-19 14:32:25 +10:00
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
Joel Beeren
Alejandro Gomez-Londono
Gerwin Klein
Rafal Kolanski
Gerwin Klein
Miki Tanaka
Matthew Brecknell
Thomas Sewell
Japheth Lim
Daniel Matichuk
deang
Andrew Boyton