> The main source of economic support seems to come from applications to
> hardware and software verification. I suspect that the impediments to
> practical verification in engineering are very similar to the
> impediments to practical verification in mathematics.
I think that there are a number of examples that show that hardware
and software verification is tenable, and will soon be practical. In our
experience at Utrecht University, where we checked the proofs a number of
protocols (of which 50% for Philips) we now know that proofchecking
is absolutely necessary if one wants to have correct proofs. Currently
verification is not yet efficient, and that is the major problem. We
want that the proofchecker can do many of the routine tasks by itself.
Based on the experience we had, I believe that proofcheckers that can
do a number of these routine tasks will become essential design and
development tools.
It should be noted that there are quite a number of groups around that
check software and hardware, and that rather large systems with complex
proofs have been verified.
Some technical data of our approach:
We used the prooftool COQ.
Some references. These can be obtained via www.phil.ruu.nl or
ftp.phil.ruu.nl
\bibitem{GroPo93}
J.F. Groote and J.C. van~de Pol.
\newblock A bounded retransmission protocol for large data packets. {A}
case study in computer checked verification.
\newblock Technical Report 100, Logic Group Preprint Series, Utrecht
University, 1993.
\bibitem{hel193b}
L.~Helmink, M.P.A. Sellink, and F.W. Vaandrager.
\newblock Proof-checking a data link protocol.
\newblock In Barendregt and Nipkow \cite{bar193a}, pages 127--165.
\bibitem{sel193a}
M.P.A. Sellink.
\newblock Verifying process algebra proofs in type theory.
\newblock Technical Report~87, Logic Group Preprint Series, Utrecht
University, March 1993.
\bibitem{bez193a}
M.A. Bezem and J.F. Groote.
\newblock A formal verification of the alternating bit protocol in the
calculus of constructions.
\newblock Technical Report~88, Logic Group Preprint Series, Utrecht
University, March 1993.
\bibitem{kor194a}
H.~Korver and J.~Springintveld.
\newblock A computer-checked verification of {M}ilner's scheduler.
\newblock In Hagiya and Mitchel {\em Proceedings of the $2^{nd}$
International Symposium on
Theoretical Aspects of Computer Software, {TACS} '94, {\rm Sendai,
Japan}}, volume 789 of {\em Lecture Notes in Compute, pages 161--178.