From owner-freebsd-hackers Sat May 15 4:52:25 1999 Delivered-To: freebsd-hackers@freebsd.org Received: from peach.ocn.ne.jp (peach.ocn.ne.jp [210.145.254.87]) by hub.freebsd.org (Postfix) with ESMTP id A905E14D03; Sat, 15 May 1999 04:52:21 -0700 (PDT) (envelope-from dcs@newsguy.com) Received: from newsguy.com by peach.ocn.ne.jp (8.9.1a/OCN) id UAA15061; Sat, 15 May 1999 20:52:15 +0900 (JST) Message-ID: <373D5F5C.4D19831F@newsguy.com> Date: Sat, 15 May 1999 20:49:48 +0900 From: "Daniel C. Sobral" X-Mailer: Mozilla 4.51 [en] (Win98; I) X-Accept-Language: pt-BR,ja MIME-Version: 1.0 To: Dag-Erling Smorgrav Cc: chat@FreeBSD.ORG, Wes Peters , hackers@FreeBSD.ORG Subject: Re: BSD, GPL, the world today. References: <199905131530.LAA04222@etinc.com> <373CB22B.4843BD45@softweyr.com> <19990515014823.A82329@catkin.nothing-going-on.org> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Content-Transfer-Encoding: 7bit Sender: owner-freebsd-hackers@FreeBSD.ORG Precedence: bulk X-Loop: FreeBSD.ORG 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: ) 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