Contract-Based Verification of MATLAB-Style Matrix Programs

Jonatan Wiik, Pontus Boström

    Forskningsoutput: TidskriftsbidragArtikelVetenskapligPeer review

    1 Citeringar (Scopus)

    Sammanfattning

    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.
    OriginalspråkOdefinierat/okänt
    Sidor (från-till)79–107
    TidskriftFormal Aspects of Computing
    Volym28
    Utgåva1
    DOI
    StatusPublicerad - 2016
    MoE-publikationstypA1 Tidskriftsartikel-refererad

    Citera det här