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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
