Industrielle Anwendungen der CP

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

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

  wenn F mathend000# unerfüllbar ( ¬∃x mathend000#), 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/