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

[Robert Watson]

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 at fledge.watson.org      Network Associates Laboratories