Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Fri, 8 Apr 94 9:34:41 EDT
From: reetz <reetz@ira.uka.de>
To: homeier@cs.ucla.edu
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: How close is practical program proving?
Message-Id: <"i80fs2.ira.958:08.03.94.07.34.49"@ira.uka.de>

Jim Grundy wrotes:

>6) Imperitive programs have state, this introduces a level of complexity not
>usually fond in traditional mathematical proofs, or even proofs of hardware
>or functional programs.

Hardware verification deals with state, as I see it. People have
often said that hardware verification is easier than program verification
because hardware has a finite number of states. Well, that depends on your
level of abstraction. Verifying a couple of 64-Bit multipliers on the
bit-level is too hard because of size. Here you would like to use data
abstraction, e.g. natural numbers. But then, "you get killed", e.g. you
get the full complexity of software verification.
Take a look at well-accepted hardware description languages (HDL) like VHDL.
They ARE just a piece of software with the full complexity of PASCAL or
whatever. It's hard to use domain-specific knowledge ("hardware always looks
like..."), because with HDLs, you get very high abstraction levels.
You might even consider hardware-software co-design. Starting at a certain
abstraction level, there's no difference in difficulty between hardware and
software verification (so I feel free to consider hardware verification 
here, because I'm dealing with it...)

Peter Homeier writes:

> c) what makes program proving so hard anyways?

So what makes hardware verification so hard anyways? ;-)
It depends on the level of abstraction coupled with the size of stuff you
what to verify. There's a trade-off. Let me put it shortly:

    low abstraction level 
==> automatically provable 
==> easy to use, but may run out of time,memory limitations of computers soon

    high abstraction level
==> not automatically provable
==> hard to use, fit into time,memeory limitations of computers, but may run
    out of time(memory? ;-) limitations of the human verifiers soon

There are a bunch of other reasons, of course. I just wanted to add this
trade-off/abstraction level view.

Ralf

(*****************************************************************************)
(*                                                                           *)
(*  Ralf Reetz                            SFB 358 of the german research     *)
(*  reetz@informatik.uni-karlsruhe.de     society (DFG)                      *)
(*                                        University of Karlsruhe, Germany   *)
(*                                                                           *)
(*                "we prove around in a ring and suppose,                    *)
(*                 the goal sits right in the middle and knows."             *)
(*                                                                           *)
(*****************************************************************************)