SMT-{LIB,COMP}

• Standard-Modellierungssprache, Syntax/Semantik-Def:

  http://smtlib.cs.uiowa.edu/standard.shtml

• Aufgabensammlung: http://smtlib.cs.uiowa.edu/benchmarks.shtml

  Modelle aus Kombinatorik, Scheduling, Hard- und Software-Verifikation, ...

  Herkunft: crafted, industrial, (random)

• Wettbewerb: http://www.smtcomp.org/
• typische Solver:
  • Z3 http://z3.codeplex.com/ (Microsoft Research)
  • Yices http://yices.csl.sri.com/ (SRI, ehem. Stanford Research Inst.)