Program models for compositional verification

Marieke Huisman, I. Aktug, D. Gurov

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

    10 Citations (Scopus)


    Compositional verification is crucial for guaranteeing the security of systems where new components can be loaded dynamically. In earlier work, we developed a compositional verification principle for control-flow properties of sequential control flow graphs with procedures. This paper discusses how the principle can be generalised to richer program models. We first present a generic program model, of which the original program model is an instantiation, and explicate under what conditions the compositional verification principle applies. We then present two other example instantiations of the generic model: with exceptional and with multi-threaded control flow, and show that for these particular instantiations the conditions hold. The program models we present are specifically tailored to our compositional verification principle; however, they are sufficiently intuitive and standard to be useful on their own. Tool support and practical application of the method are discussed.
    Original languageUndefined
    Title of host publication10th International Conference on Formal Engineering Methods
    Place of PublicationBerlin
    Number of pages20
    ISBN (Print)978-3-540-88193-3
    Publication statusPublished - 2008
    Event10th International Conference on Formal Engineering Methods, ICFEM 2008 - Kitakyushu-City, Japan
    Duration: 27 Oct 200831 Oct 2008
    Conference number: 10

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag


    Conference10th International Conference on Formal Engineering Methods, ICFEM 2008
    Abbreviated titleICFEM


    • METIS-254898
    • EWI-13856
    • IR-62491

    Cite this