Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 19 Aug 1994 17:52:59 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA12988; Fri, 19 Aug 1994 10:44:20 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA12983; Fri, 19 Aug 1994 10:44:17 -0600 Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA01274; Fri, 19 Aug 1994 10:42:30 -0600 Message-Id: <9408191642.AA01274@jaguar.cs.byu.edu> To: "P. Sreeranga Rajan" Cc: info-hol@leopard.cs.byu.edu Subject: Re: timings: Tamarack-{2,3} in HOL In-Reply-To: Your message of Tue, 16 Aug 1994 19:59:20 -0700. <9408170259.AA23453@SAIL.Stanford.EDU> Date: Fri, 19 Aug 1994 10:42:29 -0600 From: Phil Windley On Tue, 16 Aug 94 19:59:20 -0700 "P. Sreeranga Rajan" writes +-------------------- | For a statistical data point, I am interested in knowing how long | it took for someone to specify and verify Tamarack-{2,3} in HOL. | [It surely would depend on experience in using HOL.] I think there are too many variables. The most important one is what are you going to give them regarding Tamarack to start with? Someone who doesn't know the processor at all and gets only a vague description is going to take a lot longer than someone who gets to review an existing specification. One data point: I gave Mike Coe Jeff Joyces dissertation (on Tamarack 3) and my dissertation (on the Generic Interpreter Theory) and ask him to redo Tam3 with using my methodology. He didn't know anything about HOL or formal methods, and it took him about 3 months to get up to speed and get something done. I think Tam3 is a one week job for someone experienced in HOL and who has the right tools. The hardest part is the specification. Once that's done, most of the verification is more or less automatic. --phil-- __________________________________________________________________________ Phillip J. Windley, Asst. Professor | windley@cs.byu.edu Laboratory for Applied Logic | Dept. of Computer Science, TMCB 3370 | Brigham Young University | Phone: 801.378.3722 Provo UT 84602-6576 | Fax: 801.378.7775 ------------------------------------------------------------------------ If you use WWW, I'm here.