\begin{slide}{Anwendungen}

Für jede $\Sigma$-Algebra $S$ gilt:
  \begin{itemize}\itemsep 0pt
  \item Formel $F$ ist allgemeingültig
    in der \emph{freien} $\Sigma$-Algebra
  \item $\Rightarrow$ Formel $F$ ist allgemeingültig in $S$.
  \end{itemize}
Vorteil: kein Entscheidungsverfahren für  $S$ nötig

Nachteil: Umkehrung gilt nicht.

\bigskip
Anwendung bei Analyse von Programmen, Schaltkreisen:
Unterprogramme (Teilschaltungen)  als \emph{black box},

\bigskip
Roope Kaivola et al.:
\emph{Replacing Testing with Formal Verification in Intel CoreTM i7 
Processor Execution Engine Validation},
Conf. Computer Aided Verification 2009,
\url{http://dx.doi.org/10.1007/978-3-642-02658-4_32}


\end{slide}
