Date: Tue, 29 Jul 2003 11:25:49 +0200 From: Alexander Leidinger <Alexander@Leidinger.net> To: Poul-Henning Kamp <phk@phk.freebsd.dk> Cc: cvs-all@FreeBSD.org Subject: Re: 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 Message-ID: <20030729112549.4bf47e95.Alexander@Leidinger.net> In-Reply-To: <3F258C55.6090706@tcoip.com.br> References: <62633.1059304135@critter.freebsd.dk> <3F258C55.6090706@tcoip.com.br>
next in thread | previous in thread | raw e-mail | index | archive | help
On Mon, 28 Jul 2003 17:49:25 -0300 "Daniel C. Sobral" <dcs@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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20030729112549.4bf47e95.Alexander>