From: "G.B." <bauhaus@futureapps.invalid>
Subject: Re: seL4 as base of an AdaOS with some Spark proofing?
Date: Wed, 30 Jul 2014 13:55:31 +0200
Date: 2014-07-30T13:55:31+02:00 [thread overview]
Message-ID: <lramfj$68f$1@dont-email.me> (raw)
In-Reply-To: <drednZEea59sVkXO4p2dnAA@giganews.com>
On 30.07.14 12:41, Peter Chapin wrote:
> The question one must ask is: how difficult is it to do and how much
> "normal" code can you effectively prove?
Questions about the efficiency of coding/reasoning could well
be made economically interesting, I think. In this seL4
scenario, one is proving formal source text, and measuring
this effort could be done by using wall clock time (as usual),
that is: person hours, and processor time.
Looking at what they show, e.g., no buffer overflows, no
problems with arithmetic, avoiding certain pointer issues,
one could compare the difficulties of preventing these mostly
by construction, i.e., scalar types of Ada + GNATSpark, and
not by proving things after the fact.
next prev parent reply other threads:[~2014-07-30 11:55 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. [this message]
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
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