[Prev][Next][Index]

Re: A question

    From: sakthi@ba.tis.com (Sakthi Subramanian)
    Date: Fri, 20 Oct 95 10:17:02 PDT

    Hi, all! This maybe a naive question. But I have always wondered why
    one shouldn't use a proven powerful verification system such as Nqthm
    (Boyer-Moore theorem prover) for specification of programs. After all
    when you verify a program you have to express the specification of the
    program.  Nqthm has been used sucessfully to verify programs in a
    number of languages. So why not use that? Why use systems like Larch
    and LP which are specifically geared only to express specifications and
    not verification? Of course there are cosmetic differences like one is
    a typed language and the other is not, etc. But I think these can be
    ignored.

    sakthi

Sakthi,

Indeed, there are people using Nqthm for program verification (including
Yuan Yu here at Digital's Systems Research Center).  A lot depends on what
you are trying to accomplish.

One of the biggest problems for software verification is getting the
software specifications written (and then debugged) in the first place.
Our experience indicates that when dealing with software developers it
is fatal to "just ignore cosmetic differences."  If they find the
specification language unwritable (unreadable), they just won't write
specifications (or even read them).

Another obstacle to formal verification is getting a precise specification
of the language--in the logic and language of the verifier.  For a kernel
of pure Lisp, this isn't too hard.  But if you aspire to work with programs
in "real" languages, like C and Ada (or even Pascal and Modula), you will
find that this is a very difficult task.  It's not an unimportant task, it
just isn't the one that we chose for Larch.

Computational Logic, Inc. (CLInc) is engaged in pretty much the research
program you seem to be suggesting, and doing some very good work on
verifying a "trusted stack," but there is still a large gap between what
they are able to verify and what you might reasonably specify with, say,
LCL and check with LCLint.  Contact good@cli.com (Donald I. Good) for more
information about their work.

We are in no danger of running out of research problems in this area.
There's plenty of hard work to go around, and it is healthy for various
groups to tackle different parts of the problem.  (It's also healthy, from
time to time, to ask hard questions about putting the pieces together.)

Jim H.