• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Contract-Based Verification of MATLAB-Style Matrix Programs

Jonatan Wiik, Pontus Boström, Contract-Based Verification of MATLAB-Style Matrix Programs. Formal Aspects of Computing 28(1), 79–107, 2016.

http://dx.doi.org/10.1007/s00165-015-0353-z

Abstract:

MATLAB/Simulink is a popular toolset for developing embedded software. The main target of the toolset is numerical computing applications and the tools offer a rich language for manipulating matrices. This paper presents an approach to automatic, modular, contract-based verification of programs written in a subset of the MATLAB programming language. We focus on efficient handling of the built-in matrix manipulation functions commonly used in MATLAB. We restrict ourselves to the subset of MATLAB suitable for code generation, which means matrix types and shapes can be determined statically. We present an approach to static type and shape inference for matrices that is more strict than MATLAB, but aids verification. The type and shape information is then used in the verification. From the programs and contracts we generate verification conditions that are discharged with an off-the-shelf SMT solver. We discuss two approaches to encode matrix functions and evaluate them on a number of examples. We also investigate the use of k-induction to decrease the need for user annotations. We found our approach to be efficient for programs that manipulate relatively small matrices, which are common in embedded applications.

BibTeX entry:

@ARTICLE{jWiBo16a,
  title = {Contract-Based Verification of MATLAB-Style Matrix Programs},
  author = {Wiik, Jonatan and Boström, Pontus},
  journal = {Formal Aspects of Computing},
  volume = {28},
  number = {1},
  pages = {79–107},
  year = {2016},
  ISSN = {1433-299X},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 2

Edit publication