Where is verification code? #13

Closed
master-q opened this Issue Nov 4, 2015 · 2 comments

Projects

None yet

2 participants

@master-q
master-q commented Nov 4, 2015

In example of seL4, the verification code is found at https://github.com/seL4/l4v. Where is verification code of eChronos RTOS?

@lsf37
Contributor
lsf37 commented Nov 5, 2015

The specs and proofs for eChronos are not public at this stage.

Note that at this stage eChronos has only fully undergone code-level verification by model-checking to exclude undefined C behaviour. The full functional correctness verification in Isabelle/HOL is still in progress.

@lsf37 lsf37 closed this Nov 5, 2015
@master-q
master-q commented Nov 5, 2015

The specs and proofs for eChronos are not public at this stage.

I understand it. Thanks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment