First fully verified operating system kernel.
От: thesz Россия
Дата: 14.08.09 09:45
Оценка: 8 (2)

Обсуждение на слешдоте со ссылками.


The researchers used an executable specification written in Haskell, C code that mapped to the Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system.

Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Подождите ...
Пока на собственное сообщение не было ответов, его можно удалить.