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; Wed, 19 Apr 1995 20:52:37 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA033629470; Wed, 19 Apr 1995 13:24:30 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from ultrastar.EE.CORNELL.EDU by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA033569468; Wed, 19 Apr 1995 13:24:28 -0600 Date: Wed, 19 Apr 95 15:22:31 EDT From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser) Received: by ultrastar.EE.CORNELL.EDU (4.1/1.6.10+n-y-Cornell-Electrical-Engineering) id AA11510; Wed, 19 Apr 95 15:22:31 EDT Message-Id: <9504191922.AA11510@ultrastar.EE.CORNELL.EDU> To: info-hol@leopard.cs.byu.edu Subject: verifying floating point arithmetic This is a follow up on the message by Randy Bryant. I find it interesting that Randy says: ** The biggest challenge is to convert the specification of one stage, involving arithmetic expressions and inequalities, into a bit-level form. I think this shows the importance of the role of theorem proving in this context. This is the kind of things that theorem proving is good at. BDDs are most likely a better match for the binary level verification. Lifting that reasoning up to reasoning at the arithmetic level is best done by other methods.