CVPP: A Tool Set for Compositional Verification of Control-Flow Safety Properties

Marieke Huisman, Dilian Gurov

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

    9 Citations (Scopus)
    57 Downloads (Pure)

    Abstract

    This paper describes CVPP, a tool set for compositional verification of control–flow safety properties for programs with procedures. The compositional verification principle that underlies CVPP is based on maximal models constructed from component specifications. Maximal models replace the actual components when verifying the whole program, either for the purposes of modularity of verification or due to unavailability of the component implementations at verification time. A characteristic feature of the principle and the tool set is the distinction between program structure and behaviour. While behavioural properties are more abstract and convenient for specification purposes, structural ones are easier to manipulate, in particular when it comes to verification or the construction of maximal models. Therefore, CVPP also contains the means to characterise a given behavioural formula by a set of structural formulae. The paper presents the underlying framework for compositional verification and the components of the tool set. Several verification scenarios are described, as well as wrapper tools that support the automatic execution of such scenarios, providing appropriate pre– and post–processing to interface smoothly with the user and to encapsulate the inner workings of the tool set.
    Original languageEnglish
    Title of host publicationFormal Verification of Object-Oriented Software
    Subtitle of host publicationInternational Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers
    EditorsBernhard Beckert, Claude Marche
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages107-121
    Number of pages15
    ISBN (Electronic)978-3-642-18070-5
    ISBN (Print)978-3-642-18069-9
    DOIs
    Publication statusPublished - 2010
    EventInternational Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2010 - Paris, France
    Duration: 28 Jun 201030 Jun 2010

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume6528

    Conference

    ConferenceInternational Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2010
    Abbreviated titleFoVeOOS
    Country/TerritoryFrance
    CityParis
    Period28/06/1030/06/10

    Keywords

    • 2024 OA procedure

    Fingerprint

    Dive into the research topics of 'CVPP: A Tool Set for Compositional Verification of Control-Flow Safety Properties'. Together they form a unique fingerprint.

    Cite this