[isabelle-dev] Isabelle Verified Linux kernel

Tobias Nipkow 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
the moment.


> Thanks,
> David Blubaugh
> This body part will be downloaded on demand.

More information about the isabelle-dev mailing list