\begin{slide}{Industrielle Anwendungen der CP}

  \begin{itemize} \itemsep 1pt\parskip 1pt
  \item Verifikation von Schaltkreisen\\
    (\emph{bevor} man diese tatsächlich produziert)

    $F =  \text{S-Implementierung}(x) 
    \neq \text{S-Spezifikation}(x)$

    wenn $F$ unerfüllbar ($\neg \exists x$), 
    dann Implementierung 
    korrekt
  \item Verifikation von Software
    durch \emph{model checking}:

    Programmzustände abstrahieren 
    durch Zustands\-prä\-di\-kate,
    Programmabläufe durch endliche Automaten.

    z. B. Static Driver Verifier
    \url{http://research.microsoft.com/en-us/projects/slam/}

    benutzt Constraint-Solver Z3
    \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}

  \end{itemize}

\end{slide}

\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\RR}{\mathbb{R}}

