From: Peter Chapin <PChapin@vtc.vsc.edu>
Subject: Re: seL4 as base of an AdaOS with some Spark proofing?
Date: Wed, 30 Jul 2014 06:41:53 -0400
Date: 2014-07-30T06:41:53-04:00 [thread overview]
Message-ID: <drednZEea59sVkXO4p2dnAA@giganews.com> (raw)
In-Reply-To: <lracht$8a9$1@dont-email.me>
On 2014-07-30 05:06, Georg Bauhaus wrote:
> Having an OS written in C that is proven correct and available
> online shows that Ada / GNATSpark is not needed any more.
It is not news that it is possible to prove certain C programs correct.
I refer you to the Frama-C project and it's deductive verification
plugins as one example.
The question one must ask is: how difficult is it to do and how much
"normal" code can you effectively prove?
Peter
next prev parent reply other threads:[~2014-07-30 10:41 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 [this message]
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
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