In this paper we present how formal methods can be applied
to MATLAB programs. We apply a static analysis based on abstract interpretation
to derive reachable values and identify potential programming
faults fully automatically. Our verification is built on a formalization and
abstraction of matrices, structures and data types, such as integers and
IEEE-754
oats. Combined with previously presented static analysis for
Simulink, our tool can verify block diagrams with embedded MATLAB
code. We show the feasibility of our tool and compare our solutions
against a commercial tool, using real world applications.