Contract-Based Verification of MATLAB-Style Matrix Programs

Jonatan Wiik, Pontus Boström

    Research output: Contribution to journalArticleScientificpeer-review

    1 Citation (Scopus)

    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.
    Original languageUndefined/Unknown
    Pages (from-to)79–107
    JournalFormal Aspects of Computing
    Volume28
    Issue number1
    DOIs
    Publication statusPublished - 2016
    MoE publication typeA1 Journal article-refereed

    Cite this