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 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
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.
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?
If
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
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
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
code
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.
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 render
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 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
' 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) components, to
reach the level
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
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?
--
14 matches
Mail list logo
