Abstract Interpretation of MATLAB Code with Interval Sets
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
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.
Christian Dernehl, Norman Hansen,Stefan Kowalewski