\begin{slide}{Automatische Verifikation?}

Automatisches Beweisen von Programm-Eigenschaften
ist praktisch unmöglich.

(Satz von Gödel, Turing:  Halteproblem ist nicht entscheidbar.)

D. h., der Programmierer muß mithelfen:
Programm und Beweis \emph{gleichzeitig} schreiben.

Werkzeuge können verifizieren, daß beides zueinander paßt.

Simples Beispiel: Programm und Typ-Deklarationen.

\end{slide}



\begin{slide}{Verifikation als Wundermittel?}

in sicherheitskritischen Bereichen ist Verifikation Pflicht:
Schaltkreis-Herstellung, Kryptographie, Luft- und Raumfahrt

\emph{jedoch:}

man verifiziert immer nur bezüglich einer Spezifikation
und mit Hilfe von Werkzeugen:

\begin{itemize}
\item
  wer verifiziert die Spezifikation?
\item
  wer verifiziert die Werkzeuge?
\end{itemize}

siehe Lehrveranstaltungen im Hauptstudium 
(Prof. Geser, Prof. Petermann)

\end{slide}

