-----------------------------------------------------------------------

4th International Workshop on Strategies in Automated Deduction
                       (STRATEGIES 2001)

             held in conjunction with IJCAR 2001
             in Siena, Italy, June 18 / 19, 2001

-----------------------------------------------------------------------

                        INVITED TALK


      Mechanical Software Verification: High Level 
       Control Aspects from a User's Perspective

                    by Wolfgang Goerigk
       Institut für Informatik und Praktische Mathematik
       Christian-Albrechts-Universität zu Kiel, Germany 


                          Abstract

In the talk we will present lessons learned from using inductive
theorem proving for mechanical proof support in software
verification. We will use two running examples. The first is compiler
verification, and the second is an industrial project in which we
proved the partial correctness of a safety critical expert system,
using techniques of (verified) runtime result verification.

It is not our primary goal to show how to control a particular prover
(like e.g. ACL2 or PVS) to succeed and finally prove what we want.
There is a high risk either to formulate theorems which are simply not
true, or (practically) not provable, or useless. Therefore, a major
part of the talk will be on what we can and what we cannot expect to
be able to prove for a realistic piece of executable software. We will
emphasize the importance of partial program correctness and its
preservation, i.e., of a correctness guarantee for regularly computed
non-erroneous results also of machine executables. This is often
sufficient, very practical, and sometimes surprisingly easy to prove.

Software verification may succeed, although it is often considered
hard or even impossible -- in particular for large and complex
systems. Mechanical proof support can help finding proofs (and
errors). It may help to redo (or reuse) proofs after slight
modifications. And it might establish correctness. But in the latter
case we depend on the prover. Its positive results, i.e., the
succeeding proofs, should in principle be understandable and/or
checkable, manually or by trusted proof checking programs. Otherwise
we would leave a serious gap in the mechanically supported process of
correct software construction and proof documentation.

----------------------------------------------------------------------