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)

    Abstract

    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
    PublisherSpringer
    Pages136-150
    Number of pages15
    ISBN (Print)978-3-540-93899-6
    DOIs
    Publication statusPublished - 2009

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume5403

    Fingerprint

    Structural properties
    Flow graphs
    Acoustic waves

    Keywords

    • Property translation
    • Compositional verification
    • Temporal Logic

    Cite this

    Gurov, D., & Huisman, M. (2009). Reducing Behavioural to Structural Properties of Programs with Procedures. In N. D. Jones, & M. Müller-Olm (Eds.), Verification, Model Checking, and Abstract Interpretation (pp. 136-150). [10.1007/978-3-540-93900-9_14] (Lecture Notes in Computer Science; Vol. 5403). London: Springer. https://doi.org/10.1007/978-3-540-93900-9_14
    Gurov, D. ; Huisman, Marieke. / Reducing Behavioural to Structural Properties of Programs with Procedures. Verification, Model Checking, and Abstract Interpretation. editor / N.D. Jones ; M. Müller-Olm. London : Springer, 2009. pp. 136-150 (Lecture Notes in Computer Science).
    @inproceedings{83c8cbf9bb5248b0b577f09011162956,
    title = "Reducing Behavioural to Structural Properties of Programs with Procedures",
    abstract = "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.",
    keywords = "Property translation, Compositional verification, Temporal Logic",
    author = "D. Gurov and Marieke Huisman",
    year = "2009",
    doi = "10.1007/978-3-540-93900-9_14",
    language = "English",
    isbn = "978-3-540-93899-6",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "136--150",
    editor = "N.D. Jones and M. M{\"u}ller-Olm",
    booktitle = "Verification, Model Checking, and Abstract Interpretation",

    }

    Gurov, D & Huisman, M 2009, Reducing Behavioural to Structural Properties of Programs with Procedures. in ND Jones & M Müller-Olm (eds), Verification, Model Checking, and Abstract Interpretation., 10.1007/978-3-540-93900-9_14, Lecture Notes in Computer Science, vol. 5403, Springer, London, pp. 136-150. https://doi.org/10.1007/978-3-540-93900-9_14

    Reducing Behavioural to Structural Properties of Programs with Procedures. / Gurov, D.; Huisman, Marieke.

    Verification, Model Checking, and Abstract Interpretation. ed. / N.D. Jones; M. Müller-Olm. London : Springer, 2009. p. 136-150 10.1007/978-3-540-93900-9_14 (Lecture Notes in Computer Science; Vol. 5403).

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

    TY - GEN

    T1 - Reducing Behavioural to Structural Properties of Programs with Procedures

    AU - Gurov, D.

    AU - Huisman, Marieke

    PY - 2009

    Y1 - 2009

    N2 - 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.

    AB - 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.

    KW - Property translation

    KW - Compositional verification

    KW - Temporal Logic

    U2 - 10.1007/978-3-540-93900-9_14

    DO - 10.1007/978-3-540-93900-9_14

    M3 - Conference contribution

    SN - 978-3-540-93899-6

    T3 - Lecture Notes in Computer Science

    SP - 136

    EP - 150

    BT - Verification, Model Checking, and Abstract Interpretation

    A2 - Jones, N.D.

    A2 - Müller-Olm, M.

    PB - Springer

    CY - London

    ER -

    Gurov D, Huisman M. Reducing Behavioural to Structural Properties of Programs with Procedures. In Jones ND, Müller-Olm M, editors, Verification, Model Checking, and Abstract Interpretation. London: Springer. 2009. p. 136-150. 10.1007/978-3-540-93900-9_14. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-93900-9_14