Procedure-Modular Verification of Control Flow Safety Properties

Siavash Soleimanifard, Dilian Gurov, Marieke Huisman

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

    3 Citations (Scopus)
    166 Downloads (Pure)

    Abstract

    This paper describes a novel technique for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity of verification is achieved by relativizing the correctness of global properties on the local properties rather than on the implementations of methods, and is based on the construction of maximal models. Tool support is provided by means of ProMoVer, a tool that is essentially a wrapper around a previously developed tool set for compositional verification of control flow safety properties, where program data is abstracted away completely. We evaluate the technique on a small but realistic case study.
    Original languageUndefined
    Title of host publication12th Workshop on Formal Techniques for Java-like Programs, FTfJP 2010
    Place of PublicationNew York
    PublisherAssociation for Computing Machinery
    Pages5:1-5:7
    Number of pages7
    ISBN (Print)978-1-4503-0540-2
    DOIs
    Publication statusPublished - 2010
    Event12th Workshop on Formal Techniques for Java-like Programs, FTfJP 2010 - Maribor, Slovenia
    Duration: 22 Jun 201022 Jun 2010
    Conference number: 12
    https://distrinet.cs.kuleuven.be/events/ftfjp10/

    Publication series

    Name
    PublisherACM

    Workshop

    Workshop12th Workshop on Formal Techniques for Java-like Programs, FTfJP 2010
    Abbreviated titleFTfJP
    Country/TerritorySlovenia
    CityMaribor
    Period22/06/1022/06/10
    Internet address

    Keywords

    • METIS-270992
    • Modular Verification
    • Temporal Logic
    • IR-72645
    • EWI-18324
    • Maximal Models

    Cite this