From: Georg Bauhaus <bauhaus@futureapps.invalid>
Subject: Re: seL4 as base of an AdaOS with some Spark proofing?
Date: Thu, 31 Jul 2014 08:23:54 +0200
Date: 2014-07-31T08:23:54+02:00 [thread overview]
Message-ID: <lrcndq$egl$1@dont-email.me> (raw)
In-Reply-To: <lrc2of$36l$1@dont-email.me>
On 31/07/14 02:31, Simon Clubley wrote:
>> >(2) In-kernel ASM functions,
> It's not clear if they mean some assembly language kernel functions or
> if they are talking about the generated code from the compiler.
>
They explain that every kernel must have some assembly
language in it, and that theirs has some 300 lines of assembly.
Sounds like one can prove this amount of assembly code correct?
next prev parent reply other threads:[~2014-07-31 6:23 UTC|newest]
Thread overview: 16+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-07-30 8:22 seL4 as base of an AdaOS with some Spark proofing? kug1977
2014-07-30 9:06 ` Georg Bauhaus
2014-07-30 10:41 ` Peter Chapin
2014-07-30 11:55 ` G.B.
2014-07-30 17:47 ` Shark8
2014-07-30 22:40 ` Peter Chapin
2014-07-30 22:53 ` Shark8
2014-07-31 0:31 ` Simon Clubley
2014-07-31 6:23 ` Georg Bauhaus [this message]
2014-07-30 17:58 ` anon
2014-07-31 22:03 ` gvdschoot
2014-08-01 7:42 ` kug1977
2014-08-01 8:27 ` gvdschoot
2014-08-01 9:04 ` gvdschoot
2014-08-01 19:32 ` Randy Brukardt
2014-08-01 19:17 ` anon
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox