From owner-cvs-src@FreeBSD.ORG  Sun Jul 27 06:27:42 2003
Return-Path: <owner-cvs-src@FreeBSD.ORG>
Delivered-To: cvs-src@freebsd.org
Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125])
	by hub.freebsd.org (Postfix) with ESMTP
	id EA39937B401; Sun, 27 Jul 2003 06:27:42 -0700 (PDT)
Received: from fledge.watson.org (fledge.watson.org [204.156.12.50])
	by mx1.FreeBSD.org (Postfix) with ESMTP
	id F3E3643FBF; Sun, 27 Jul 2003 06:27:40 -0700 (PDT)
	(envelope-from robert@fledge.watson.org)
Received: from fledge.watson.org (localhost [127.0.0.1])
	by fledge.watson.org (8.12.9/8.12.9) with ESMTP id h6RDQqai050074;
	Sun, 27 Jul 2003 09:26:52 -0400 (EDT)
	(envelope-from robert@fledge.watson.org)
Received: from localhost (robert@localhost)h6RDQq17050071;
	Sun, 27 Jul 2003 09:26:52 -0400 (EDT)
Date: Sun, 27 Jul 2003 09:26:52 -0400 (EDT)
From: Robert Watson <rwatson@freebsd.org>
X-Sender: robert@fledge.watson.org
To: Alexander Leidinger <Alexander@Leidinger.net>
In-Reply-To: <20030727115457.553f1df7.Alexander@Leidinger.net>
Message-ID: <Pine.NEB.3.96L.1030727091934.49952A-100000@fledge.watson.org>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
cc: cvs-src@freebsd.org
cc: Poul-Henning Kamp <phk@phk.freebsd.dk>
cc: src-committers@freebsd.org
cc: dds@freebsd.org
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
X-BeenThere: cvs-src@freebsd.org
X-Mailman-Version: 2.1.1
Precedence: list
List-Id: CVS commit messages for the src tree <cvs-src.freebsd.org>
List-Unsubscribe: <http://lists.freebsd.org/mailman/listinfo/cvs-src>,
	<mailto:cvs-src-request@freebsd.org?subject=unsubscribe>
List-Archive: <http://lists.freebsd.org/pipermail/cvs-src>
List-Post: <mailto:cvs-src@freebsd.org>
List-Help: <mailto:cvs-src-request@freebsd.org?subject=help>
List-Subscribe: <http://lists.freebsd.org/mailman/listinfo/cvs-src>,
	<mailto:cvs-src-request@freebsd.org?subject=subscribe>
X-List-Received-Date: Sun, 27 Jul 2003 13:27:43 -0000


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