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)
    136 Downloads (Pure)


    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
    Number of pages8
    ISBN (Electronic)978-3-030-03418-4
    ISBN (Print)978-3-030-03417-7
    Publication statusPublished - 2018
    Event8th International Symposium, ISoLA 2018 - Royal Apollonia Beach Hotel, Limassol, Cyprus
    Duration: 5 Nov 20189 Nov 2018
    Conference number: 8

    Publication series

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


    Conference8th International Symposium, ISoLA 2018
    Abbreviated titleISoLA 2018
    Internet address


    Dive into the research topics of 'On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification'. Together they form a unique fingerprint.

    Cite this