Reducing Behavioural to Structural Properties of Programs with Procedures

D. Gurov, Marieke Huisman

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

    6 Citations (Scopus)


    There is an intimate link between program structure and behaviour. Exploiting this link to phrase program correctness problems in terms of the structural properties of a program graph rather than in terms of its unfoldings is a useful strategy for making analyses more tractable. This paper presents a characterisation of behavioural program properties through sets of structural properties by means of a translation. The characterisation is given in the context of a program model based on control flow graphs of sequential programs with possibly recursive procedures, and properties expressed in a fragment of the modal \mu-calculus with boxes and greatest fixed-points only. The property translation is based on a tableau construction that conceptually amounts to symbolic execution of the behavioural formula, collecting structural constraints along the way. By keeping track of the subformulae that have been examined, recursion in the structural constraints can be identified and captured by fixed-point formulae. The tableau construction terminates, and the characterisation is exact, i.e., the translation is sound and complete. A prototype implementation has been developed. We discuss several applications of the characterisation, in particular compositional verification for behavioural properties, based on maximal models.
    Original languageEnglish
    Title of host publicationVerification, Model Checking, and Abstract Interpretation
    EditorsN.D. Jones, M. Müller-Olm
    Place of PublicationLondon
    Number of pages15
    ISBN (Print)978-3-540-93899-6
    Publication statusPublished - 2009

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag


    • Property translation
    • Compositional verification
    • Temporal Logic

    Fingerprint Dive into the research topics of 'Reducing Behavioural to Structural Properties of Programs with Procedures'. Together they form a unique fingerprint.

    Cite this