design flaws. So we have only removed 50% of the problem.
for my part there have been many, many days when I would settle for
solving 50% of a problem
-gunnar
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscript
Caveats on the proofs, as I recall. I'll try to dig up the details.
It's been pretty extensively discussed elsewhere...
On Fri, Oct 2, 2009 at 12:54 PM, Dimitri DeFigueiredo
wrote:
> There is a proof for a whole kernel I can use today. How's that not
> practically useful? Is it not practically
There is a proof for a whole kernel I can use today. How's that not practically
useful? Is it not practically useful because there are caveats on the proof? I
don't we can just dismiss this one without further reasoning or because we
don't know how to apply it to our own problems.
Dimitri
> My $.02... I don't think this approach is going to catch on anytime soon.
> Spending 30 or so staff years verifying a 7500 line C program is not going
> to be seen as cost effective by most real-world managers. But interesting
> research nonetheless.
maybe not as crazy as it sounds: this is a mi
At 4:33 PM -0500 10/1/09, Wall, Kevin wrote:
> "Professor Gernot Heiser, the John Lions Chair in Computer Science in
> the School of Computer Science and Engineering and a senior principal
> researcher with NICTA, said for the first time a team had been able to
> prove with mathema
I have a few concerns with formal proofs particularly applying them in a
non-academic environment (some of which may be my own naïve lack of
understanding and my feeble memory of my university years studying formal
methods).
Firstly whilst the code provably does what you said that it would do, tha
This was discussed a few months ago on several other lists I read.
The consensus is that it's interesting, and is further than anyone
else has gone in recent years to do proofs, but not practically
useful. Additionally, there are a lot of caveats on the proof (which
I don't recall, but are well do
Thought there might be several on this list who might appreciate
this, at least from a theoretical perspective but had not seen
it. (Especially Larry Kilgallen, although he's probably already seen it. :)
In
http://www.unsw.edu.au/news/pad/articles/2009/sep/microkernel_breakthrough.html,
"Pro
