Date: Sun, 27 Jul 2003 09:26:52 -0400 (EDT) From: Robert Watson <rwatson@freebsd.org> To: Alexander Leidinger <Alexander@Leidinger.net> 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: <Pine.NEB.3.96L.1030727091934.49952A-100000@fledge.watson.org> In-Reply-To: <20030727115457.553f1df7.Alexander@Leidinger.net>
next in thread | previous in thread | raw e-mail | index | archive | help
On Sun, 27 Jul 2003, Alexander Leidinger wrote: > > We still have no tools which help us translate high level abstractions > > into low level code or for that matter to validate the high level > > abstractions in the first place. > > Are you talking about e.g. model checking? After Aug 2 I plan to look at > porting 2 major open source model checkers. Last time I used NuSMV, it ran just fine on FreeBSD. That was in 1999, though. But porting model checkers has never been the hard part of model checking to software development, it's finding the models that hurts... I can't help wondering if the single most positive step in the direction of having formalism and analysis tools available in development wouldn't be to use a language other than C... :-) Robert N M Watson FreeBSD Core Team, TrustedBSD Projects robert@fledge.watson.org Network Associates Laboratories
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?Pine.NEB.3.96L.1030727091934.49952A-100000>