[isabelle-dev] Isabelle Verified Linux kernel
nipkow at in.tum.de
Wed Oct 5 06:07:02 CEST 2011
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 proving of software system SS?
Isabelle is not a model checker. There have been experiments in linking
Isabelle up with model checkers but I am not aware of a stable link at
> David Blubaugh
> This body part will be downloaded on demand.
More information about the isabelle-dev