ProMoVer: Modular Verification of Temporal Safety Properties.

Siavash Soleimanifard, Dilian Gurov, Marieke Huisman

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

    5 Citations (Scopus)

    Abstract

    This paper describes ProMoVer, a tool 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 at the procedure–level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations, and is based here on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre– and post–processing. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light–weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the smart card domain.
    Original languageUndefined
    Title of host publicationProceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011)
    EditorsGilles Barthe, Alberto Pardo, Gerardo Schneider
    Place of PublicationBerlin
    PublisherSpringer
    Pages366-381
    Number of pages16
    ISBN (Print)978-3-642-24690-6
    DOIs
    Publication statusPublished - Nov 2011
    Event9th International Conference on Software Engineering and Formal Methods, SEFM 2011 - Montevideo, Uruguay
    Duration: 14 Nov 201118 Nov 2011
    Conference number: 9

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume7041

    Conference

    Conference9th International Conference on Software Engineering and Formal Methods, SEFM 2011
    Abbreviated titleSEFM
    CountryUruguay
    CityMontevideo
    Period14/11/1118/11/11

    Keywords

    • METIS-281578
    • EWI-20830
    • IR-78615

    Cite this