Am 05/10/2011 00:23, schrieb David Blubaugh:
> Has anyone ever developed a verified and validated version of the Linux
> kernel by utilizing the Isabelle / HOL environment ??
Not that I have heard about it ;-)
>
> Does Isabelle support non-determinsitic model checking as well as
> theorem prov
Has anyone ever developed a verified and validated version of the Linux kernel
by utilizing the Isabelle / HOL environment ??
Would anybody be interested in developing such a kernel ??
Does Isabelle support non-determinsitic model checking as well as theorem
proving of software system
