This paper presents an approach to automatic, modular, contract-based verification of programs written in a subset of the MATLAB programming language, with focus on efficiently handling the provided matrix manipulation functions. We statically infer types and shapes for matrices in the language and use this information in the verification. We consider two approaches for verification: direct axiomatisation of the built-in matrix functions and expansion of the functions. We evaluate our approaches on a number of examples and discuss challenges for automatic verification in this setting.
CITATION STYLE
Wiik, J., & Boström, P. (2014). Contract-based verification of MATLAB and simulink matrix-manipulating code. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8829, pp. 396–412). Springer Verlag. https://doi.org/10.1007/978-3-319-11737-9_26
Mendeley helps you to discover research relevant for your work.