http://www.nicta.com.au/news/home_page_content_listing/world-first_research_breakthrough_promises_safety-critical_software_of_unprecedented_reliability
NICTA announced the completion of the worlds first formal machine-checked
proof of a general-purpose operating system kernel, promising safety-c
在 Thu, 20 Aug 2009 16:56:24 +0800，Kagamin 写道:
http://www.nicta.com.au/news/home_page_content_listing/world-first_research_breakthrough_promises_safety-critical_software_of_unprecedented_reliability
NICTA announced the completion of the world’s first formal
machine-checked proof of a general-
davidl Wrote:
> If so, they may need to further proof the compiler always
> generate correct binaries.
And that the processor doesn't have flaws either. This is what's called an
unprecedented level of reliability, I believe.
Kagamin wrote:
NICTA announced the completion of the world’s first formal machine-checked
proof of a general-purpose operating system kernel, promising safety-critical
software of unprecedented levels of reliability.
Yes, sort of what they proved was that the implementation was inline
with t
