Things change, computer dev evolves too
openbsd dev team uses audit code with great success
but many industrial domains uses new technics like static analysis with
success too
for exemple in avionics soft : astrée is a tool that certified Airbus plane
software with static analysis
read astree web
On Thu, 19 Sep 2013, josef.win...@email.de wrote:
> Does OpenBSD plan to varify its (main) components, to reach the level of
> zero-bug software?
Just out of curiousity, how much verifying would it take to reach the
level of "zero-bug software"?
How would that affect the development cycle?
>
On Thu, 19 Sep 2013, Peter N. M. Hansteen wrote:
> I remain unconvinced that it's possible to formally verify non-trivial
> code to be bug free. You remain free to convince me otherwise or point
> me to available verified non-trivial software roughly on par with a
> complete operating system.
Pre
On 9/19/13 9:29 PM, josef.win...@email.de wrote:
Does OpenBSD plan to varify its (main) components, to
reach the level of zero-bug software?
I do assume that you are talking about "formal verification" meaning
"mathematical proof of correctness".
Verify against what? Verification is a binary
pe...@bsdly.net (Peter N. M. Hansteen) writes:
> systems that have developed in response to real-world needs and formal
> standards specifications that at least in some cases more likely than
> not were in any way verified even to be internally consistent.
missing a 'never' in there. clearer?
-
josef.win...@email.de writes:
> Right, a varified full flaged OS is still future.
> But there is nevertheless progress and affort.
Thanks for the pointeres, but anytime this comes up, an old AI
witticism turns up at the back of my head,
"If our mind were so simple we could actually u
eless' out of your annoying
signature? it would fit in a single line.
I've never heard of Wired 4G LTE network.
> From: josef.winger@email.deSent: Thursday, September 19, 2013 4:30 PMTo:
> misc@openbsd.orgSubject: Verified OS concerns
>
> Does OpenBSD plan to varify its (main)
On 09/19/2013 04:29 PM, josef.win...@email.de wrote:
Does OpenBSD plan to varify its (main) components, to
reach the level of zero-bug software?
you mean, painfully reviewing and auditing code?
what do you think they've been trying to do for the last 15 years?
And after that, they have been try
On Thu, Sep 19, 2013 at 22:29, josef.win...@email.de wrote:
> Does OpenBSD plan to varify its (main) components, to
> reach the level of zero-bug software?
>
> If not, isn't there any concern that (future) varified OS
> will render OBSD redundant one day?
Short answer: no. Long answer: still no.
On Thu, Sep 19, 2013 at 10:29:39PM +0200, josef.win...@email.de wrote:
> Does OpenBSD plan to varify its (main) components, to
> reach the level of zero-bug software?
No. Zeno convinced us that you can't get there from here.
>
> If not, isn't there any concern that (future) varified OS
> will re
On Thu, Sep 19, 2013 at 05:14:37PM -0400, Nick Holland wrote:
> Don't get me wrong, I'd love to see a general purpose OS with the
> basic reliability of my car,
Actually, it looks more and more like the reverse is coming true.
josef.win...@email.de writes:
> Does OpenBSD plan to varify its (main) components, to
> reach the level of zero-bug software?
>
> If not, isn't there any concern that (future) varified OS
> will render OBSD redundant one day?
I remain unconvinced that it's possible to formally verify non-trivial
Interesting thread...
Sent from my BlackBerry 10 smartphone on the Verizon Wireless 4G LTE
network.
From: josef.winger@email.deSent: Thursday, September 19, 2013 4:30 PMTo:
misc@openbsd.orgSubject: Verified OS concerns
Does OpenBSD plan to varify its (main) components, to
reach the level of zero
Does OpenBSD plan to varify its (main) components, to
reach the level of zero-bug software?
If not, isn't there any concern that (future) varified OS
will render OBSD redundant one day?
/jo
14 matches
Mail list logo
