Skip site navigation (1)Skip section navigation (2)
Date:      Sat, 15 May 1999 20:49:48 +0900
From:      "Daniel C. Sobral" <dcs@newsguy.com>
To:        Dag-Erling Smorgrav <des@flood.ping.uio.no>
Cc:        chat@FreeBSD.ORG, Wes Peters <wes@softweyr.com>, hackers@FreeBSD.ORG
Subject:   Re: BSD, GPL, the world today.
Message-ID:  <373D5F5C.4D19831F@newsguy.com>
References:  <199905131530.LAA04222@etinc.com> <xlxso8z2w76.fsf@gold.cis.ohio-state.edu> <373CB22B.4843BD45@softweyr.com> <19990515014823.A82329@catkin.nothing-going-on.org> <xzpiu9u39kq.fsf@localhost.ping.uio.no>

next in thread | previous in thread | raw e-mail | index | archive | help
Dag-Erling Smorgrav wrote:
> 
> Correctness proofs are very time-consuming, because they can't be
> automated. There are experimental tools which can assist with part of
> the work (e.g. the partially-completed Abel project at the University
> of Oslo: <URL:http://www.ifi.uio.no/~prover/abel/>) but the hardest
> part of the job - finding loop and type invariants and post- and
> pre-conditions which the prover can use as starting points - must
> still be done manually.

Things like SPIN goes a long, long way to make such proofs more
viable. Take, for instance, correctness proofs of Fluke IPC
subsystem.

--
Daniel C. Sobral			(8-DCS)
dcs@newsguy.com
dcs@freebsd.org

	"Proof of Trotsky's farsightedness is that _none_ of his
predictions have come true yet."


To Unsubscribe: send mail to majordomo@FreeBSD.org
with "unsubscribe freebsd-chat" in the body of the message




Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?373D5F5C.4D19831F>