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)
    27 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