Industrielle Anwendungen der CP

• Verifikation von Schaltkreisen
  (bevor man diese tatsächlich produziert)

  F = S-Implementierung(x)≠S-Spezifikation(x)

  wenn F unerfüllbar ( ¬∃x), dann Implementierung korrekt

• Verifikation von Software durch model checking:

  Programmzustände abstrahieren durch Zustandsprädikate, Programmabläufe durch endliche Automaten.

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

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