[isabelle-dev] Isabelle Verified Linux kernel

[David Blubaugh]

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 SS?  
 
Thanks,
 
David Blubaugh

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20111004/4f067e83/attachment.html>