From: Mitchell@cs.Stanford.EDU (John C. Mitchell)
Date: Mon, 16 Sep 1996 15:08:19 -0700
Subject: Re: Why did software verification die?

At 12:26 PM 9/16/96, Paul E. Black wrote:
>>From the late 1960's to the early 1980's software verification was
>a thriving field: new inference methods were developed, tools (like
>the Stanford Pascal Verifier) were developed, PhD's granted, and so
>forth.  Since then it seems that little has happened: verifiers
>aren't part of industry's tool kit, computer science students rarely
>use verification (and even less often, verifiers), etc.  What
>happened?
>

OK. I'll take a wild shot at this. Here's my extreme position:

1) Verification is hard. But when there is an adequate incentive to
be sure about correctness, some combination of verification and testing
is worthwhile.

2) There were and still are significant language and semantics issues.
The early work was almost all on first-order languages -- Pascal does
not allow procedure parameters that have procedure parameters. When you
try to go beyond that, you get into lots of questions about semantic models.
That has taken a long time to explore.

3) The lofty goal of complete verification is too ambitious.
Set your sights lower, and you'll have a better chance of success.

4) I'll wager that the next 10 years see a significant turnaround in this
area, with some aspects of specification and verification becoming
mainstream commercial techniques.

John

Go to messages for September 1996 or latest