Program Correctness by Transformation

Marieke Huisman, Stefan Blom, Saeed Darabi, Mohsen Safari

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    2 Citations (Scopus)
    37 Downloads (Pure)

    Abstract

    Deductive program verification can be used effectively to verify high-level programs, but can be challenging for low-level, high-performance code. In this paper, we argue that compilation and program transformations should be made annotation-aware, i.e. during compilation and program transformation, not only the code should be changed, but also the corresponding annotations. As a result, if the original high-level program could be verified, also the resulting low-level program can be verified. We illustrate this approach on a concrete case, where loop annotations that capture possible loop parallelisations are translated into specifications of an OpenCL kernel that corresponds to the parallel loop. We also sketch how several commonly used OpenCL kernel transformations can be adapted to also transform the corresponding program annotations. Finally, we conclude the paper with a list of research challenges that need to be addressed to further develop this approach.
    Original languageEnglish
    Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Modeling
    Subtitle of host publication8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I
    EditorsTiziana Margaria, Bernhard Steffen
    Place of PublicationCham
    PublisherSpringer
    Pages365-380
    Number of pages16
    ISBN (Electronic)978-3-030-03418-4
    ISBN (Print)978-3-030-03417-7
    DOIs
    Publication statusPublished - 2018
    Event8th International Symposium, ISoLA 2018 - Royal Apollonia Beach Hotel, Limassol, Cyprus
    Duration: 5 Nov 20189 Nov 2018
    Conference number: 8
    http://www.isola-conference.org/isola2018/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume11244
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference8th International Symposium, ISoLA 2018
    Abbreviated titleISoLA 2018
    CountryCyprus
    CityLimassol
    Period5/11/189/11/18
    Internet address

      Fingerprint

    Cite this

    Huisman, M., Blom, S., Darabi, S., & Safari, M. (2018). Program Correctness by Transformation. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I (pp. 365-380). (Lecture Notes in Computer Science; Vol. 11244). Cham: Springer. https://doi.org/10.1007/978-3-030-03418-4_22