Dynamic Frames Based Verification Method for Concurrent Java Programs

Wojciech Mostowski

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

    4 Citations (Scopus)
    82 Downloads (Pure)

    Abstract

    In this paper we discuss a verification method for concurrent Java programs based on the concept of dynamic frames. We build on our earlier work that proposes a new, symbolic permission system for concurrent reasoning and we provide the following new contributions. First, we describe our approach for proving program specifications to be self-framed w.r.t. permissions, which is a necessary condition to maintain soundness in concurrent reasoning. Second, we show how we use predicates to provide modular and reusable specifications for program synchronisation points, like locks or forked threads. Our work primarily targets the KeY verification system with its specification language JML* and symbolic execution proving method. Hence, we also give the current status of the work on implementation and we discuss some examples that are verifiable with KeY.
    Original languageEnglish
    Title of host publicationProceedings of the 7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015. Revised Selected Papers
    EditorsArie Gurfinkel, Sanjit A. Seshia
    Place of PublicationCham
    PublisherSpringer
    Pages124-141
    Number of pages18
    ISBN (Electronic)978-3-319-29613-5
    ISBN (Print)978-3-319-29612-8
    DOIs
    Publication statusPublished - 2016
    Event7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015 - San Francisco, United States
    Duration: 18 Jul 201519 Jul 2015
    Conference number: 7

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer International Publishing Switzerland
    Volume9593
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015
    Abbreviated titleVSTTE
    CountryUnited States
    CitySan Francisco
    Period18/07/1519/07/15

    Keywords

    • JML
    • Java
    • Dynamic frames
    • Interactive verification
    • Symbolic permissions
    • Permission accounting

    Fingerprint

    Dive into the research topics of 'Dynamic Frames Based Verification Method for Concurrent Java Programs'. Together they form a unique fingerprint.

    Cite this