On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification

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

    1 Citation (Scopus)
    10 Downloads (Pure)

    Abstract

    Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.
    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
    Pages111-118
    Number of pages8
    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

    Cite this

    Huisman, M. (2018). On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification. 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. 111-118). (Lecture Notes in Computer Science; Vol. 11244). Cham: Springer. https://doi.org/10.1007/978-3-030-03418-4_7
    Huisman, Marieke. / On Models and Code : A Unified Approach to Support Large-Scale Deductive Program Verification. Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. editor / Tiziana Margaria ; Bernhard Steffen. Cham : Springer, 2018. pp. 111-118 (Lecture Notes in Computer Science).
    @inproceedings{e00e7414f3474e0cb69ec6119213a8d7,
    title = "On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification",
    abstract = "Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.",
    author = "Marieke Huisman",
    year = "2018",
    doi = "10.1007/978-3-030-03418-4_7",
    language = "English",
    isbn = "978-3-030-03417-7",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "111--118",
    editor = "Tiziana Margaria and Bernhard Steffen",
    booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Modeling",

    }

    Huisman, M 2018, On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification. 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. Lecture Notes in Computer Science, vol. 11244, Springer, Cham, pp. 111-118, 8th International Symposium, ISoLA 2018, Limassol, Cyprus, 5/11/18. https://doi.org/10.1007/978-3-030-03418-4_7

    On Models and Code : A Unified Approach to Support Large-Scale Deductive Program Verification. / Huisman, Marieke.

    Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. ed. / Tiziana Margaria; Bernhard Steffen. Cham : Springer, 2018. p. 111-118 (Lecture Notes in Computer Science; Vol. 11244).

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

    TY - GEN

    T1 - On Models and Code

    T2 - A Unified Approach to Support Large-Scale Deductive Program Verification

    AU - Huisman, Marieke

    PY - 2018

    Y1 - 2018

    N2 - Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.

    AB - Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.

    UR - http://www.scopus.com/inward/record.url?scp=85056476794&partnerID=8YFLogxK

    U2 - 10.1007/978-3-030-03418-4_7

    DO - 10.1007/978-3-030-03418-4_7

    M3 - Conference contribution

    SN - 978-3-030-03417-7

    T3 - Lecture Notes in Computer Science

    SP - 111

    EP - 118

    BT - Leveraging Applications of Formal Methods, Verification and Validation. Modeling

    A2 - Margaria, Tiziana

    A2 - Steffen, Bernhard

    PB - Springer

    CY - Cham

    ER -

    Huisman M. On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. Cham: Springer. 2018. p. 111-118. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-03418-4_7