Contract-Based Verification of MATLAB-Style Matrix Programs

Jonatan Wiik, Pontus Boström

    Tutkimustuotos: LehtiartikkeliArtikkeliTieteellinenvertaisarvioitu

    1 Sitaatiot (Scopus)

    Abstrakti

    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.
    AlkuperäiskieliEi tiedossa
    Sivut79–107
    JulkaisuFormal Aspects of Computing
    Vuosikerta28
    Numero1
    DOI - pysyväislinkit
    TilaJulkaistu - 2016
    OKM-julkaisutyyppiA1 Julkaistu artikkeli, soviteltu

    Viittausmuodot