cvs commit: src/sys/kern init_main.c kern_malloc.c md5c.c subr_autoconf.c subr_mbuf.c subr_prf.c tty_subr.c vfs_cluster.c vfs_subr.c

[Alexander Leidinger]

On Mon, 28 Jul 2003 17:49:25 -0300
"Daniel C. Sobral" <dcs at tcoip.com.br> wrote:

> Poul-Henning Kamp wrote:
> > 
> > Yes I think it would, but you would have to find a way to prove to 
> > yourself that your model was in fact precise and faithful relative to
> > the kernel source.
> > 
> > I'm still hoping that some day we will have tools which will read
> > source code and alert us to things which doesn't make sense or which
> > looks dubious.
> 
> Well, that's what I like about Spin. A clever use of macros let you 
> pre-process your C code to be "Spinnable" with little to no work. :-)

BTW. it's the second model checker I want to add a port for, I just
hadn't the URL at hand at the time I mentioned uppaal. See
http://spinroot.com/spin/whatispin.html for more.

Bye,
Alexander.

-- 
                   Press every key to continue.

http://www.Leidinger.net                       Alexander @ Leidinger.net
  GPG fingerprint = C518 BC70 E67F 143F BE91  3365 79E2 9C60 B006 3FE7