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-hackers" 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>