[isabelle-dev] Isabelle Verified Linux kernel

[Tobias Nipkow]

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.

Best
Tobias

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