ist ein System zur statischen Analyse von Source Code. Lizenzgeber ist die Firma „The MathWorks“.

Zur Interpretation des Programmcode wird eine Abstraktion verwendet.  Sie ermöglicht die Prüfung der Wertebereiche von Variablen. Diese Eigenschaft wird genutzt um typische Laufzeitfehler wie z.B. Division by Zero oder Array Access out of Bounds zu finden.