Static Code Verification Through Process Models

Sebastiaan J. C. Joosten, Marieke Huisman

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

    44 Downloads (Pure)

    Abstract

    In this extended abstract, we combine two techniques for program verification: one is Hoare-style static verification, and the other is model checking of state transition systems. We relate the two techniques semantically through the use of a ghost variable. Actions that are performed by the program can be logged into this variable, building an event structure as its value. We require the event structure to grow incrementally by construction, giving it behavior suitable for model checking. Invariants specify a correspondence between the event structure and the program state. The combined power of model checking and static code verification with separation logic based reasoning, gives a new and intuitive way to do program verification. We describe our idea in a tool-agnostic way: we do not give implementation details, nor do we assume that the static verification tool to which our idea might apply is implemented in a particular way.
    Original languageEnglish
    Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Distributed Systems
    Subtitle of host publication8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III
    EditorsTiziana Margaria, Bernhard Steffen
    Place of PublicationCham
    PublisherSpringer
    Pages343-354
    Number of pages12
    ISBN (Electronic)978-3-030-03424-5
    ISBN (Print)978-3-030-03423-8
    DOIs
    Publication statusPublished - 31 Oct 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
    Volume11246
    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 Dive into the research topics of 'Static Code Verification Through Process Models'. Together they form a unique fingerprint.

    Cite this